Theorems · Theorem · group theory

AddSubgroup.map_addCommutator

∀ {G : Type u_1} {G' : Type u_2} [inst : AddGroup G] [inst_1 : AddGroup G'] (H₁ H₂ : AddSubgroup G) (f : G →+ G'),
  AddSubgroup.map f ⁅H₁, H₂⁆ = ⁅AddSubgroup.map f H₁, AddSubgroup.map f H₂⁆

Defined in

Mathlib.GroupTheory.Commutator.Basic

Cited by

6 results in Mathlib

Foundations

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

Assumes

AddGroupAddGroup