trinomial_natTrailingDegree — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

theorem trinomial_natTrailingDegree (hkm : k < m) (hmn : m < n) (hu : u ≠ 0) :
    (trinomial k m n u v w).natTrailingDegree = k :=
  by
  refine
    natTrailingDegree_eq_of_trailingDegree_eq_some
      ((Finset.le_inf fun i h => ?_).antisymm <|
          trailingDegree_le_of_ne_zero <| by rwa [trinomial_trailing_coeff' hkm hmn]).symm
  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 le_rfl
  · exact WithTop.coe_le_coe.mpr hkm.le
  · exact WithTop.coe_le_coe.mpr (hkm.trans hmn).le

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