trinomial_natDegree — Mathlib

English

If k < m < n and w ≠ 0, then natDegree of trinomial k m n u v w equals n.

Русский

Если k < m < n и w ≠ 0, то natDegree триномии равен n.

LaTeX

$$$$ \\operatorname{natDegree}(\\operatorname{trinomial}(k,m,n,u,v,w)) = n. $$$$

Lean4

theorem trinomial_natDegree (hkm : k < m) (hmn : m < n) (hw : w ≠ 0) : (trinomial k m n u v w).natDegree = n :=
  by
  refine
    natDegree_eq_of_degree_eq_some
      ((Finset.sup_le fun i h => ?_).antisymm <| le_degree_of_ne_zero <| by rwa [trinomial_leading_coeff' hkm hmn])
  replace h := support_trinomial' k m n u v w h
  rw [mem_insert, mem_insert, mem_singleton] at h
  rcases h with (rfl | rfl | rfl)
  · exact WithBot.coe_le_coe.mpr (hkm.trans hmn).le
  · exact WithBot.coe_le_coe.mpr hmn.le
  · exact le_rfl

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