funext_of_le_card — Mathlib

English

If F is homogeneous of degree n and eval r F = 0 for all r, and n ≤ |R|, then F = 0.

Русский

Если F однороден степени n и eval r F = 0 при всех r и n ≤ |R|, тогда F = 0.

LaTeX

$$IsHomogeneous(F, n) → (∀ r, eval r F = 0) → n ≤ |R| → F = 0$$

Lean4

/-- See `MvPolynomial.IsHomogeneous.funext`
for a version that assumes `Infinite R`. -/
theorem funext_of_le_card (hF : F.IsHomogeneous n) (hG : G.IsHomogeneous n) (h : ∀ r : σ → R, eval r F = eval r G)
    (hnR : n ≤ #R) : F = G := by
  rw [← sub_eq_zero]
  apply eq_zero_of_forall_eval_eq_zero_of_le_card (hF.sub hG) _ hnR
  simpa [sub_eq_zero] using h

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