English
Let R be an infinite commutative ring. If F and G are homogeneous polynomials of degree n in the multivariate polynomial ring MvPolynomial(σ, R), and eval_r F = eval_r G for every r : σ → R, then F = G.
Русский
Пусть R — бесконечное коммутативное кольцо. Пусть F и G — однородные многочлены по степени n в кольце многочленов MvPolynomial(σ, R). Если для любой подстановки r: σ → R выполнения eval_r F = eval_r G, то F = G.
LaTeX
$$$\\text{Infinite }R \\Rightarrow \\forall F,G,\\; (F \\text{ and } G \\text{ are homogeneous of degree } n) \\wedge (\\forall r:\\, \\sigma \\to R,\\; \\mathrm{eval}_r F = \\mathrm{eval}_r G) \\Rightarrow F = G$$$
Lean4
/-- See `MvPolynomial.IsHomogeneous.funext_of_le_card`
for a version that assumes `n ≤ #R`. -/
theorem funext [Infinite R] {F G : MvPolynomial σ R} {n : ℕ} (hF : F.IsHomogeneous n) (hG : G.IsHomogeneous n)
(h : ∀ r : σ → R, eval r F = eval r G) : F = G :=
by
apply funext_of_le_card hF hG h
exact (Cardinal.nat_lt_aleph0 _).le.trans <| Cardinal.infinite_iff.mp ‹Infinite R›
