mul_sub_algebraMap_pow_commutes — Mathlib

English

For any x ∈ A, r ∈ R, and n ≥ 0, x · (x − algebraMap_R A r)^n = (x − algebraMap_R A r)^n · x; i.e., the same commutation holds for powers.

Русский

Для любых x ∈ A, r ∈ R и n ≥ 0 выполняется x·(x − algebraMap_R A r)^n = (x − algebraMap_R A r)^n·x; та же коммутативность применяется к степеням.

LaTeX

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

Lean4

theorem mul_sub_algebraMap_pow_commutes [Ring A] [Algebra R A] (x : A) (r : R) (n : ℕ) :
    x * (x - algebraMap R A r) ^ n = (x - algebraMap R A r) ^ n * x := by
  induction n with
  | zero => simp
  | succ n ih => rw [pow_succ', ← mul_assoc, mul_sub_algebraMap_commutes, mul_assoc, ih, ← mul_assoc]

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