Monomorphism_Image_is_Isomorphic_to_Domain
Provedhomomorphismsisomorphismsproofwiki
An injective group homomorphism gives a bijection from the domain to the image.
Preamble
import Mathlib.Algebra.Group.Hom.Defs import Mathlib.Data.Set.Function
Formal statement
theorem Monomorphism_Image_is_Isomorphic_to_Domain {G H : Type _} [Group G] [Group H] (f : MonoidHom G H) (hinj : Function.Injective f) : Function.Bijective (fun g : G => (⟨f g, Set.mem_range.mpr ⟨g, rfl⟩⟩ : Set.range f)) := by sorrySource