Theorems · Definition · group theory

AddMonoidHom.rangeRestrict

{G : Type u_1} → [inst : AddGroup G] → {N : Type u_5} → [inst_1 : AddGroup N] → (f : G →+ N) → G →+ ↥f.range

The canonical surjective AddGroup homomorphism G →+ f(G) induced by a group homomorphism G →+ N.

Defined in

Mathlib.Algebra.Group.Subgroup.Ker

Cited by

14 results in Mathlib

Foundations

Depth 23 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

AddGroupAddGroup