center_eq_top — Mathlib

English

For a commutative semigroup M, the center equals the top element; i.e., every element commutes with every other.

Русский

Для коммутативной полугруппы M центр совпадает с верхней степенью, то есть каждый элемент коммутирует с каждым другим.

LaTeX

$$$ center\\ M = ⊤ $$$

Lean4

@[to_additive (attr := simp)]
theorem center_eq_top : center M = ⊤ :=
  SetLike.coe_injective (Set.center_eq_univ M)

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