degree_C

Mathlib.RingTheory.MvPolynomial.MonomialOrder

URI: https://scilib.ai/kg/mathlib#MonomialOrder.degree_C

English

For any constant r, the degree of its constant polynomial is zero.

Русский

Для константы r степень соответствующего константного полинома равна нулю.

LaTeX

$$$\deg_m(C(r)) = 0$$$

Lean4

@[simp]
theorem degree_C (r : R) : m.degree (C r) = 0 := by rw [degree_eq_zero_iff_totalDegree_eq_zero, totalDegree_C]

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

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

Разделы

Аффилиация

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