NPAへ戻る
Declaration
ring_image_intro
Mathlib.Algebra.Ring.FirstIsomorphism.Basic
Packages
2
Module
63
Theorem
750
Declarations
1016
信頼境界外の sidecar
Source text や表示 overlay は提示用メタデータです。信頼する証拠は署名済み証明書と checker の結果です。
Statement
forall (R : Sort u), forall (S : Sort v), forall (f : forall (x : R), S), forall (a : R), @RingImagePred.{u,v} R S f (f a)Proof term
theorem ring_image_intro.{u,v} :
forall (R : Sort u), forall (S : Sort v), forall (f : forall (x : R), S), forall (a : R), @RingImagePred.{u,v} R S f (f a) :=
fun R => fun S => fun f => fun a => @image_intro.{u,v} R S f a