Theorems · Definition · group theory

AddSubgroup.comap

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

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

Defined in

Mathlib.Algebra.Group.Subgroup.Map

Cited by

123 results in Mathlib

Foundations

Depth 21 from the axioms, rests on 106 definitions · uses propext

Assumes

AddGroupAddGroup