le_centralizer_iff_isMulCommutative

English

For a subgroup K of G, K ≤ centralizer(K) if and only if K is multiplicatively commutative (abelian).

Русский

Для подгруппы K в G верно: K ≤ centralizer(K) тогда и только тогда, когда K абелево.

LaTeX

$$K \le centralizer(K) \iff IsMulCommutative K$$

Lean4

@[to_additive]
theorem le_centralizer_iff_isMulCommutative : K ≤ centralizer K ↔ IsMulCommutative K :=
  ⟨fun h => ⟨⟨fun x y => Subtype.ext (h y.2 x x.2)⟩⟩, fun h x hx y hy => congr_arg Subtype.val (h.1.1 ⟨y, hy⟩ ⟨x, hx⟩)⟩

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