degree_add_of_lt — Mathlib

English

If deg g ≺ deg f, then deg(f+g) = deg f.

Русский

Если deg g меньше deg f по порядку, то deg(f+g) = deg f.

LaTeX

$$$m.degree g \prec_m m.degree f \Rightarrow m.degree (f+g) = m.degree f$$$

Lean4

theorem degree_add_of_lt {f g : MvPolynomial σ R} (h : m.degree g ≺[m] m.degree f) : m.degree (f + g) = m.degree f :=
  by
  apply m.toSyn.injective
  apply le_antisymm
  · apply le_trans degree_add_le
    simp only [sup_le_iff, le_refl, true_and, le_of_lt h]
  · apply le_degree
    rw [mem_support_iff, coeff_add, m.coeff_eq_zero_of_lt h, add_zero, ← leadingCoeff, leadingCoeff_ne_zero_iff]
    intro hf
    rw [← not_le, hf] at h
    apply h
    simp only [degree_zero, map_zero]
    apply bot_le

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