English
For all R commutative semirings, if q.IsHomogeneous n and hpq: aeval ![X,1] q = p, then p.homogenize n = q.
Русский
Пусть R — коммутативное полуринг, тогда если qIsHomogeneous n и hpq: aeval ![X,1] q = p, то p.homogenize n = q.
LaTeX
$$$\\forall n\\ n\\IsHomogeneous\\ q \\Rightarrow (\\operatorname{aeval} ![X,1] q = p \\Rightarrow p^{\\mathrm{hom}}_n = q).$$$
Lean4
/-- `(x + y)^n` can be expressed as `x^n + n*x^(n-1)*y + k * y^2` for some `k` in the ring.
-/
def powAddExpansion {R : Type*} [CommSemiring R] (x y : R) :
∀ n : ℕ, { k // (x + y) ^ n = x ^ n + n * x ^ (n - 1) * y + k * y ^ 2 }
| 0 => ⟨0, by simp⟩
| 1 => ⟨0, by simp⟩
| n + 2 => by
obtain ⟨z, hz⟩ := (powAddExpansion x y (n + 1))
exists x * z + (n + 1) * x ^ n + z * y
calc
(x + y) ^ (n + 2) = (x + y) * (x + y) ^ (n + 1) := by ring
_ = (x + y) * (x ^ (n + 1) + ↑(n + 1) * x ^ (n + 1 - 1) * y + z * y ^ 2) := by rw [hz]
_ = x ^ (n + 2) + ↑(n + 2) * x ^ (n + 1) * y + (x * z + (n + 1) * x ^ n + z * y) * y ^ 2 :=
by
push_cast
ring!
