degree_C

Mathlib.Algebra.Polynomial.Degree.Definitions

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

← MathLib Explorer

English

If a ≠ 0, then the degree of the constant polynomial C(a) is 0.

Русский

Если a ≠ 0, то deg(C(a)) = 0.

LaTeX

$$degree(C(a)) = 0 \\,\\text{for } a \\neq 0$$

Lean4

@[simp]
theorem degree_C (ha : a ≠ 0) : degree (C a) = (0 : WithBot ℕ) := by
  rw [degree, ← monomial_zero_left, support_monomial 0 ha, max_eq_sup_coe, sup_singleton, WithBot.coe_zero]

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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