powSubPowFactor — Mathlib

English

The same existence claim as Pow Add Expansion, with the auxiliary unfoldings describing the explicit form of the equality for each n.

Русский

Та же самая утверждение существования, что и в Pow Add Expansion, с подробным развертыванием равенства по каждому $n$.

LaTeX

$$$\\text{For all } x,y \\in R, \\exists k ∈ R\\; (x+y)^n = x^n + n x^{n-1} y + k y^2 \\text{ for each } n. $$$

Lean4

/-- `x^n - y^n` can be expressed as `z * (x - y)` for some `z` in the ring.
-/
def powSubPowFactor (x y : R) : ∀ i : ℕ, { z : R // x ^ i - y ^ i = z * (x - y) }
  | 0 => ⟨0, by simp⟩
  | 1 => ⟨1, by simp⟩
  | k + 2 => by
    obtain ⟨z, hz⟩ := @powSubPowFactor x y (k + 1)
    exists z * x + y ^ (k + 1)
    linear_combination (norm := ring) x * hz

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