eq_zero_of_forall_eval_eq_zero — Mathlib

English

If F is homogeneous of degree n and eval r F = 0 for all r, then F = 0 (version with infinite base ring).

Русский

Если F однороден степени n и eval r F = 0 при всех r, тогда F = 0 (бессмысленно для бесконечной базы R).

LaTeX

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

Lean4

/-- See `MvPolynomial.IsHomogeneous.eq_zero_of_forall_eval_eq_zero_of_le_card`
for a version that assumes `n ≤ #R`. -/
theorem eq_zero_of_forall_eval_eq_zero [Infinite R] {F : MvPolynomial σ R} {n : ℕ} (hF : F.IsHomogeneous n)
    (h : ∀ r : σ → R, eval r F = 0) : F = 0 :=
  by
  apply eq_zero_of_forall_eval_eq_zero_of_le_card hF h
  exact (Cardinal.nat_lt_aleph0 _).le.trans <| Cardinal.infinite_iff.mp ‹Infinite R›

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