proposition: Theorem grp_first_iso : A / grp_kernel phi ≅ grp_image phi.
proof: Proof. exact (Build_GroupIsomorphism _ _ grp_image_quotient _). Defined.
imports: Basics Types Truncations.Core Algebra.Congruence Algebra.Groups.Group Algebra.Groups.Subgroup Algebra.Groups.Image Algebra.Groups.Kernel Colimits.Quotient HSet Spaces.Finite.Finite WildCat Modalities.Modality