eq_zero_of_eval_eq_zero — Mathlib

English

Let p be a polynomial in R(σ, K) with the property that eval v p = 0 for all v: σ → K and suppose p ∈ restrictDegree(σ, K, |K| − 1). Then p = 0.

Русский

Пусть p ∈ R(σ, K) удовлетворяет eval v p = 0 для всех v: σ → K и p ∈ restrictDegree(σ, K, |K| − 1). Тогда p = 0.

LaTeX

$$$$ p = 0 \\\\text{ if } (\\\\forall v: σ \\\\to K, \\\\mathrm{eval}(v, p) = 0) \\\\land p \\in R(\\\\sigma, K). $$$$

Lean4

theorem eq_zero_of_eval_eq_zero [Finite σ] (p : MvPolynomial σ K) (h : ∀ v : σ → K, eval v p = 0)
    (hp : p ∈ restrictDegree σ K (Fintype.card K - 1)) : p = 0 :=
  let p' : R σ K := ⟨p, hp⟩
  have : p' ∈ ker (evalᵢ σ K) := funext h
  show p'.1 = (0 : R σ K).1 from congr_arg _ <| by rwa [ker_evalₗ, mem_bot] at this

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