degree_C

Mathlib.Algebra.Polynomial.Laurent

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

English

For any a ∈ R with a ≠ 0, the degree of the constant Laurent monomial C a is 0.

Русский

Для любого a ∈ R, a ≠ 0, степень константного лаурентового монома C a равна 0.

LaTeX

$$$\forall a \in R,\ a \neq 0\Rightarrow (C(a)).degree = 0$$$

Lean4

theorem degree_C {a : R} (a0 : a ≠ 0) : (C a).degree = 0 :=
  by
  rw [← mul_one (C a), ← T_zero]
  exact degree_C_mul_T 0 a a0

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

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

Разделы

Аффилиация

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