algebraMap_mem_center — Mathlib

English

For every r in R, the element algebraMap R A r lies in the center of A (it commutes with every element of A).

Русский

Для каждого r ∈ R элемент algebraMap R A r лежит в центре A (он коммутирует с каждым элементом A).

LaTeX

$$$\forall r \in R,\; algebraMap R A r \in \operatorname{Center}(A)$$$

Lean4

theorem _root_.Set.algebraMap_mem_center (r : R) : algebraMap R A r ∈ Set.center A := by
  simp only [Semigroup.mem_center_iff, commutes, forall_const]

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