degree_add_of_ne — Mathlib

English

If deg f ≠ deg g, then deg(f+g) equals the supremum of deg f and deg g.

Русский

Если deg f ≠ deg g, то deg(f+g) равно верхней границе deg f и deg g.

LaTeX

$$$m.degree f \neq m.degree g \Rightarrow m.degree (f+g) = \text{sup}(m.degree f, m.degree g)$$$

Lean4

theorem degree_add_of_ne {f g : MvPolynomial σ R} (h : m.degree f ≠ m.degree g) :
    m.toSyn (m.degree (f + g)) = m.toSyn (m.degree f) ⊔ m.toSyn (m.degree g) :=
  by
  by_cases h' : m.degree g ≺[m] m.degree f
  · simp [degree_add_of_lt h', le_of_lt h']
  · rw [not_lt, le_iff_eq_or_lt, Classical.or_iff_not_imp_left, EmbeddingLike.apply_eq_iff_eq] at h'
    rw [add_comm, degree_add_of_lt (h' h), right_eq_sup]
    simp only [le_of_lt (h' h)]

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