mul_neg_geom_sum₂ — Mathlib

English

In a commutative ring R, for any x, y and natural n, x − y divides x^n − y^n.

Русский

В коммутативном кольце R для любых x, y и натурального n выполняется: x − y делит x^n − y^n.

LaTeX

$$$\\displaystyle x - y \\;|\\; x^n - y^n$$$

Lean4

theorem mul_neg_geom_sum₂ (h : Commute x y) (n : ℕ) :
    ((y - x) * ∑ i ∈ range n, x ^ i * y ^ (n - 1 - i)) = y ^ n - x ^ n :=
  by
  apply op_injective
  simp only [op_mul, op_sub, op_pow]
  simp [(Commute.op h.symm).geom_sum₂_mul n]

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