map_subtype_commutator — Mathlib

English

The image under the inclusion map of the commutator subgroup of H equals the commutator of H with itself, i.e. (commutator H).map H.subtype = [H,H].

Русский

Образ коммутаторной подгруппы H при включении H → G равен коммутатору H в H, т. е. (commutator H).map H.subtype = [H,H].

LaTeX

$$$ (\\mathrm{Subgroup.map}\\ H.\\mathrm{subtype}) (\\mathrm{commutator}(H)) = ⁅H,H⁆ $$$

Lean4

theorem map_subtype_commutator (H : Subgroup G) : (_root_.commutator H).map H.subtype = ⁅H, H⁆ := by
  rw [_root_.commutator_def, map_commutator, ← MonoidHom.range_eq_map, H.range_subtype]

Похожие утверждения