Theorems · Theorem · group theory

AddSubgroup.map_map

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

Defined in

Mathlib.Algebra.Group.Subgroup.Map

Cited by

6 results in Mathlib

Foundations

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

Assumes

AddGroupAddGroupAddGroup