first_iso_phi_hits_image

Mathlib.Algebra.Group.FirstIsomorphism

Packages

Module

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 (G : Sort succ u), forall (H : Sort succ v), forall (f : forall (x : G), H), forall (q : @KerQuot.{u,v} G H f), @ImagePred.{succ u,succ v} G H f (@KerQuotToH.{u,v} G H f q)

Proof term

fun G => fun H => fun f => @Quotient.indProp.{u} G (@KerSetoid.{u,v} G H f) (fun (q : @KerQuot.{u,v} G H f) => @ImagePred.{succ u,succ v} G H f (@KerQuotToH.{u,v} G H f q)) (fun (a : G) => @image_intro.{succ u,succ v} G H f a)

Constants

Mathlib.Algebra.Group.Image.ImagePred

Interface hash: sha256:894af4db85e62276c0c5a65a2b8fc6556403e76ef1c3c52e43c99c2831613e75

Mathlib.Algebra.Group.Kernel.Quotient.KerQuot

Interface hash: sha256:860face55dbec0818c0d0aed68c1fe0e65dd7de77271f509ba95949348c0b9f4

Mathlib.Algebra.Group.Kernel.Quotient.KerQuotToH

Interface hash: sha256:a6ba09fc274f34820e843708693ff210a4f7853713023922b527c3cc787b4b9e