center_eq_top — Mathlib

English

For a commutative base algebra, the center of A over R is the whole algebra, i.e., the center equals the top subalgebra.

Русский

Для коммутативной основы центр A над R равен всей алгебре; центр совпадает с верхней подалгеброй.

LaTeX

$$$ \\text{center_eq_top} : \\mathrm{center} \\; R \\; A = \\top $$$

Lean4

@[simp]
theorem center_eq_top (A : Type*) [CommSemiring A] [Algebra R A] : center R A = ⊤ :=
  SetLike.coe_injective (Set.center_eq_univ A)

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