English
Let p be a polynomial over a semiring R and a an element of R. Then the natural degree of p plus the constant polynomial C(a) is the same as the natural degree of p, i.e. natDegree(p + C a) = natDegree(p).
Русский
Пусть p — полином над полуполем R, а a ∈ R. Тогда натуральная степень(p + C(a)) равна натуральной степени p, то есть natDegree(p + C a) = natDegree(p).
LaTeX
$$$\operatorname{natDegree}(p + C a) = \operatorname{natDegree}(p)$$$
Lean4
@[simp]
theorem natDegree_add_C {a : R} : (p + C a).natDegree = p.natDegree :=
by
rcases eq_or_ne p 0 with rfl | hp
· simp
by_cases hpd : p.degree ≤ 0
· rw [eq_C_of_degree_le_zero hpd, ← C_add, natDegree_C, natDegree_C]
· rw [not_le, degree_eq_natDegree hp, Nat.cast_pos, ← natDegree_C a] at hpd
exact natDegree_add_eq_left_of_natDegree_lt hpd
