center_eq_top — Mathlib

English

An element z lies in the center of A exactly when z commutes with every element of A.

Русский

Элемент z принадлежит центру A тогда и только тогда, когда z коммутирует с каждым элементом A.

LaTeX

$$z ∈ center R A ↔ ∀ b ∈ A, b z = z b$$

Lean4

@[simp]
theorem center_eq_top (A : Type*) [NonUnitalCommSemiring A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] :
    center R A = ⊤ :=
  SetLike.coe_injective (Set.center_eq_univ A)

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