center — Mathlib

English

The center in the NonUnitalStarSubalgebra sense coincides with the center in the underlying set sense.

Русский

Центр внутри NonUnitalStarSubalgebra R A совпадает с центром в базовом множестве A.

LaTeX

$$$(center\\ R\\ A) = Set.center\\ A$$$

Lean4

/-- The center of a non-unital star algebra is the set of elements which commute with every element.
They form a non-unital star subalgebra. -/
def center : NonUnitalStarSubalgebra R A
    where
  toNonUnitalSubalgebra := NonUnitalSubalgebra.center R A
  star_mem' := Set.star_mem_center

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