English
Let R be a commutative semiring, S a commutative semiring, p ∈ R[X], n ∈ ℕ with natDegree p ≤ n, f: R →+* S, g: Fin 2 → S, and hg: g(1) = 1. Then eval₂ f g (p.homogenize n) = p.eval₂ f (g(0)).
Русский
Пусть R и S — коммутативные полуринги, p ∈ R[X], n ∈ ℕ с deg(p) ≤ n, f: R →+* S, g: Fin 2 → S, hg: g(1) = 1. Тогда eval₂ f g (p.homogenize n) = p.eval₂ f (g(0)).
LaTeX
$$$\\operatorname{eval}_2 f g (p:\\mathrm{homogenize}\\ n) = p_{\\mathrm{eval}}(f, g_0),$ где конкретнее $g_1=1$ и $p$ оценивается через $f$ над $g_0$.$$
Lean4
theorem eval₂_homogenize_of_eq_one {S : Type*} [CommSemiring S] {p : R[X]} {n : ℕ} (hn : natDegree p ≤ n) (f : R →+* S)
(g : Fin 2 → S) (hg : g 1 = 1) : MvPolynomial.eval₂ f g (p.homogenize n) = p.eval₂ f (g 0) :=
by
apply
Polynomial.induction_with_natDegree_le (fun p ↦ MvPolynomial.eval₂ f g (p.homogenize n) = p.eval₂ f (g 0)) (N := n)
· simp
· simp +contextual [hg]
· simp +contextual
· assumption
