natDegree_C_add — Mathlib

English

For any polynomial p and any a ∈ R, the natural degree of C(a) + p equals the natural degree of p, i.e. natDegree(C a + p) = natDegree(p).

Русский

Для любого полинома p и любого a ∈ R, натуральная степень C(a) + p равна степени p, то есть natDegree(C a + p) = natDegree(p).

LaTeX

$$$\operatorname{natDegree}(C a + p) = \operatorname{natDegree}(p)$$$

Lean4

@[simp]
theorem natDegree_C_add {a : R} : (C a + p).natDegree = p.natDegree := by simp [add_comm _ p]

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