centralizer_univ — Mathlib

English

Under commutativity assumptions, the centralizer of any S is the whole ambient set.

Русский

При заданных условиях коммутативности, центральизатор любого S равен всему множеству.

LaTeX

$$$ \mathrm{centralizer}(S) = \mathrm{univ} $ under commutativity assumptions$$

Lean4

@[to_additive (attr := simp) addCentralizer_univ]
theorem centralizer_univ : centralizer univ = center M :=
  Subset.antisymm (fun _ ha ↦ Semigroup.mem_center_iff.mpr fun b ↦ ha b (Set.mem_univ b)) fun _ ha b _ ↦
    (ha.comm b).symm

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