dim_le_natDegree_of_root — Mathlib

English

If p ∈ A[X] is nonzero and pb.gen is a root of p under aeval, then pb.dim ≤ natDegree(p).

Русский

Если p ≠ 0 и pb.gen — корень p по aeval, то dim(pb) ≤ natDegree(p).

LaTeX

$$∃ p ∈ A[X], p ≠ 0 ∧ aeval(pb.gen, p) = 0 ⇒ pb.dim ≤ p.natDegree$$

Lean4

theorem dim_le_natDegree_of_root (pb : PowerBasis A S) {p : A[X]} (ne_zero : p ≠ 0) (root : aeval pb.gen p = 0) :
    pb.dim ≤ p.natDegree := by
  refine le_of_not_gt fun hlt => ne_zero ?_
  rw [p.as_sum_range' _ hlt, Finset.sum_range]
  refine Fintype.sum_eq_zero _ fun i => ?_
  simp_rw [aeval_eq_sum_range' hlt, Finset.sum_range, ← pb.basis_eq_pow] at root
  have := Fintype.linearIndependent_iff.1 pb.basis.linearIndependent _ root
  rw [this, monomial_zero_right]

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