centralizer_eq_univ — Mathlib

English

If the ambient semigroup M is commutative, then the centralizer of any subset S is the whole M.

Русский

Если M коммутативно, то центральizатор любого подмножества S равен всему M.

LaTeX

$$$ \text{If } M \text{ is commutative, then } \mathrm{centralizer}(S) = \mathrm{univ}$$$

Lean4

@[to_additive (attr := simp) addCentralizer_eq_univ]
theorem centralizer_eq_univ : centralizer S = univ :=
  eq_univ_of_forall fun _ _ _ ↦ mul_comm _ _

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