Theorems · Definition · group theory

AddSubgroup.map

{G : Type u_1} → [inst : AddGroup G] → {N : Type u_5} → [inst_1 : AddGroup N] → (G →+ N) → AddSubgroup G → AddSubgroup N

The image of an AddSubgroup along an AddMonoid homomorphism is an AddSubgroup.

Defined in

Mathlib.Algebra.Group.Subgroup.Map

Cited by

189 results in Mathlib

Foundations

Depth 20 from the axioms, rests on 110 definitions · uses propext

Assumes

AddGroupAddGroup