Theorems · Theorem · group theory

AddEquiv.map_range_nsmulAddMonoidHom

∀ {M : Type u_5} {N : Type u_6} [inst : AddCommGroup M] [inst_1 : AddCommGroup N] (e : M ≃+ N) (n : ℕ),
  AddSubgroup.map (↑e) (nsmulAddMonoidHom n).range = (nsmulAddMonoidHom n).range

Defined in

Mathlib.Algebra.Group.Subgroup.Ker

Cited by

1 results in Mathlib

Foundations

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

Assumes

AddCommGroupAddCommGroup