commutes — Mathlib

English

The base ring element commutes with any element of the algebra: algebraMap R A r · x = x · algebraMap R A r.

Русский

Элемент базового кольца коммутирует с любым элементом алгебры: a r · x = x · a r.

LaTeX

$$$\operatorname{algebraMap}(R,A)(r)\,x = x\,\operatorname{algebraMap}(R,A)(r)$$$

Lean4

/-- `mul_comm` for `Algebra`s when one element is from the base ring. -/
theorem commutes (r : R) (x : A) : algebraMap R A r * x = x * algebraMap R A r :=
  Algebra.commutes' r x

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