natDegree_eq_of_natDegree_add_eq_zero

English

If natDegree(p+q) = 0, then natDegree(p) = natDegree(q).

Русский

Если natDegree(p+q) = 0, тогда natDegree(p) = natDegree(q).

LaTeX

$$$natDegree(p + q) = 0 \Rightarrow natDegree(p) = natDegree(q)$$$

Lean4

theorem natDegree_eq_of_natDegree_add_eq_zero (p q : R[X]) (H : natDegree (p + q) = 0) : natDegree p = natDegree q :=
  by
  by_cases h₁ : natDegree p = 0; on_goal 1 => by_cases h₂ : natDegree q = 0
  · exact h₁.trans h₂.symm
  · apply natDegree_eq_of_natDegree_add_lt_right; rwa [H, Nat.pos_iff_ne_zero]
  · apply natDegree_eq_of_natDegree_add_lt_left; rwa [H, Nat.pos_iff_ne_zero]

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