divX — Mathlib

English

For x,y ∈ R and i ∈ ℕ, there exists z ∈ R such that x^i − y^i = z · (x − y).

Русский

Для любых x,y ∈ R и i ∈ ℕ существует z ∈ R, такой что x^i − y^i = z · (x − y).

LaTeX

$$$\\exists z ∈ R, \\; x^i - y^i = z \\cdot (x - y)$.$$

Lean4

/-- `divX p` returns a polynomial `q` such that `q * X + C (p.coeff 0) = p`.
  It can be used in a semiring where the usual division algorithm is not possible -/
def divX (p : R[X]) : R[X] :=
  ⟨AddMonoidAlgebra.divOf p.toFinsupp 1⟩

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