Theorems · Definition · group theory

AddEquiv.addSubmonoidMap

{M : Type u_1} →
  {N : Type u_2} →
    [inst : AddZeroClass M] →
      [inst_1 : AddZeroClass N] → (e : M ≃+ N) → (S : AddSubmonoid M) → ↥S ≃+ ↥(AddSubmonoid.map e S)

An AddEquiv φ between two additive monoids M and N induces an AddEquiv between a submonoid S ≤ M and the submonoid φ(S) ≤ N. See AddMonoidHom.addSubmonoidMap for a variant for AddMonoidHoms.

Defined in

Mathlib.Algebra.Group.Submonoid.Operations

Cited by

3 results in Mathlib

Foundations

Depth 22 from the axioms · uses propext, Quot.sound

Assumes

AddZeroClassAddZeroClass