Theorems · Theorem · group theory

AddMonoidHom.map_range

∀ {G : Type u_1} [inst : AddGroup G] {N : Type u_5} {P : Type u_6} [inst_1 : AddGroup N] [inst_2 : AddGroup P]
  (g : N →+ P) (f : G →+ N), AddSubgroup.map g f.range = (g.comp f).range

Defined in

Mathlib.Algebra.Group.Subgroup.Ker

Cited by

5 results in Mathlib

Foundations

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

Assumes

AddGroupAddGroupAddGroup