center_toNonUnitalSubalgebra — Mathlib

English

Equality between centers as subalgebras and as sets holds in the nonunital star setting.

Русский

Эквивалентность центров как подпалгебры и как множества в неединичной звездной обстановке.

LaTeX

$$$\\mathrm{center}\\_{R}A\\;\\text{as Subalgebra} = \\mathrm{center}\\_{R}A\\;\\text{as Set}$$$

Lean4

@[simp]
theorem center_toNonUnitalSubalgebra : (center R A).toNonUnitalSubalgebra = NonUnitalSubalgebra.center R A :=
  rfl

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