natDegree_mul_C

Mathlib.Algebra.Polynomial.Degree.Lemmas

URI: https://scilib.ai/kg/mathlib#Polynomial.natDegree_mul_C

English

For p and a ≠ 0, natDegree (p * C a) = natDegree p.

Русский

Для p и a ≠ 0, natDegree(p * C a) = natDegree p.

LaTeX

$$$a \neq 0 \Rightarrow \operatorname{natDegree}(p * C a) = \operatorname{natDegree}(p)$$$

Lean4

theorem natDegree_mul_C (a0 : a ≠ 0) : (p * C a).natDegree = p.natDegree := by simp only [natDegree, degree_mul_C a0]

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru