English
If F and G are homogeneous of the same degree n and agree on all evaluations, then F = G, provided n ≤ |R| or a cardinal bound holds.
Русский
Если F и G однородны степени n и совпадают при всех подстановках, то F = G, при условии кардиналного ограничения.
LaTeX
$$IsHomogeneous(F, n) → IsHomogeneous(G, n) → (∀ r, eval r F = eval r G) → le n # R → F = G$$
Lean4
/-- See `MvPolynomial.IsHomogeneous.eq_zero_of_forall_eval_eq_zero`
for a version that assumes `Infinite R`. -/
theorem eq_zero_of_forall_eval_eq_zero_of_le_card (hF : F.IsHomogeneous n) (h : ∀ r : σ → R, eval r F = 0)
(hnR : n ≤ #R) : F = 0 := by
contrapose! h
obtain ⟨k, f, hf, F, rfl⟩ := exists_fin_rename F
have hF₀ : F ≠ 0 := by rintro rfl; simp at h
have hF : F.IsHomogeneous n := by rwa [rename_isHomogeneous_iff hf] at hF
obtain ⟨r, hr⟩ := exists_eval_ne_zero_of_totalDegree_le_card_aux hF hF₀ hnR
obtain ⟨r, rfl⟩ := (Function.factorsThrough_iff _).mp <| (hf.factorsThrough r)
use r
rwa [eval_rename]
