mul_sub_algebraMap_commutes — Mathlib

English

For any x ∈ A and r ∈ R, x · (x − algebraMap_R A r) = (x − algebraMap_R A r) · x; i.e., x commutes with the shifted element x − algebraMap(r).

Русский

Для любого x ∈ A и r ∈ R выполняется x · (x − algebraMap_R A r) = (x − algebraMap_R A r) · x; элемент x коммутирует с x − algebraMap(r).

LaTeX

$$x * (x - algebraMap R A r) = (x - algebraMap R A r) * x$$

Lean4

theorem mul_sub_algebraMap_commutes [Ring A] [Algebra R A] (x : A) (r : R) :
    x * (x - algebraMap R A r) = (x - algebraMap R A r) * x := by rw [mul_sub, ← commutes, sub_mul]

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