commutator_mem_commutatorSet — Mathlib

English

Let H ≤ G. The image of the commutator subgroup of H under the inclusion map H → G equals the commutator of H with itself inside G.

Русский

Пусть H ⊆ G. Образ коммутаторной подгруппы H под включением H → G равен коммутатору H внутри G.

LaTeX

$$$ (\\mathrm{Subgroup.map}\, H.\\mathrm{subtype})(\\mathrm{commutator}(\\mathrm{Subtype}\\; [x \\in H])) = ⁅H,H⁆ $$$

Lean4

theorem commutator_mem_commutatorSet : ⁅g₁, g₂⁆ ∈ commutatorSet G :=
  ⟨g₁, g₂, rfl⟩

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