Back to NPA
Declaration
ring_image_intro
Mathlib.Algebra.Ring.FirstIsomorphism.Basic
Packages
2
Module
63
Theorems
750
Declarations
1016
Untrusted sidecar
Source text and display overlays are presentation metadata. The signed certificate and checker result are the trusted evidence.
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