commutator_eq_bot_iff_le_centralizer

English

The commutator [H1,H2] equals the bottom subgroup if and only if H1 is contained in the centralizer of H2.

Русский

Коммутатор [H1,H2] равен нулю тогда и только тогда, когда H1 ⊆ центризатор H2.

LaTeX

$$$$ [H_1, H_2] = \\emptyset \\iff H_1 \\le \\operatorname{centralizer}(H_2). $$$$

Lean4

theorem commutator_eq_bot_iff_le_centralizer : ⁅H₁, H₂⁆ = ⊥ ↔ H₁ ≤ centralizer H₂ :=
  by
  rw [eq_bot_iff, commutator_le]
  refine forall_congr' fun p => forall_congr' fun _hp => forall_congr' fun q => forall_congr' fun hq => ?_
  rw [mem_bot, commutatorElement_eq_one_iff_mul_comm, eq_comm]

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