degreeOf_le_totalDegree

Stream: Is there code for X?

[Johan Commelin]

This seems to be missing... I would love to see a 1-line proof

import Mathlib

variable {R σ : Type*} [CommRing R]

lemma MvPolynomial.degreeOf_le_totalDegree (φ : MvPolynomial σ R) (i : σ) :
    φ.degreeOf i ≤ φ.totalDegree := by
  sorry

[Johan Commelin]

Ok, I got a proof

lemma MvPolynomial.degreeOf_le_iff {n : σ} {f : MvPolynomial σ R} {d : ℕ} :
    degreeOf n f ≤ d ↔ ∀ m ∈ support f, m n ≤ d := by
  simp only [← Nat.lt_succ_iff, degreeOf_lt_iff (Nat.succ_pos _)]

lemma MvPolynomial.degreeOf_le_totalDegree {σ : Type*} (φ : MvPolynomial σ R) (i : σ) :
    φ.degreeOf i ≤ φ.totalDegree := by
  rw [degreeOf_le_iff]
  intro d hd
  refine le_trans ?_ (le_totalDegree hd)
  if hi : i ∈ d.support
  then
    exact Finset.single_le_sum (fun _ _ ↦ zero_le') hi
  else
    rw [Finsupp.not_mem_support_iff] at hi
    simp only [hi, zero_le]

[Johan Commelin]

As a consequence, I now have a sorry-free proof of

lemma MvPolynomial.IsHomogeneous.exists_eval_ne_zero_of_totalDegree_le_card
    {σ : Type*} [IsDomain R]
    (F : MvPolynomial σ R) (n : ℕ)
    (hF₀ : F ≠ 0) (hF : F.IsHomogeneous n) (hn₀ : n ≠ 0) (h : n ≤ #R) :
    ∃ r : σ → R, eval r F ≠ 0

[Junyan Xu]

There is docs#MvPolynomial.restrictTotalDegree_le_restrictDegree which you can combine with mem_restrictDegree, docs#MvPolynomial.degreeOf_lt_iff etc. and maybe get a shorter proof.

[Riccardo Brasca]

You can remove n \neq 0, right? If F is homogeneous of degree 0 it is constant.

[Johan Commelin]

Good point

[Yaël Dillies]

I have this somewhere but I don't remember where :thinking: Maybe LeanCamCombi?