English
If f is injective, there exists a multiplicative isomorphism between G and its range f(G).
Русский
Если f инъективен, существует мультипликативное изоморфное отображение между G и его образом f(G).
LaTeX
$$$$ f \\text{ injective} \\;\Longrightarrow\\; G \\cong_* f(G) $$$$
Lean4
/-- The range of an injective group homomorphism is isomorphic to its domain. -/
@[to_additive /-- The range of an injective additive group homomorphism is isomorphic to its
domain. -/
]
noncomputable def ofInjective {f : G →* N} (hf : Function.Injective f) : G ≃* f.range :=
MulEquiv.ofBijective (f.codRestrict f.range fun x => ⟨x, rfl⟩)
⟨fun _ _ h => hf (Subtype.ext_iff.mp h), by
rintro ⟨x, y, rfl⟩
exact ⟨y, rfl⟩⟩
