degree_zero

Mathlib.Algebra.Polynomial.Laurent

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

English

For any n ∈ ℤ, the degree of T^n in R[T;T^{-1}] is n (for nontrivial R).

Русский

Для любого n ∈ ℤ степень T^n в R[T;T^{-1}] равна n (при ненулевом R).

LaTeX

$$$\forall n \in \mathbb Z,\ (T^{n})^{\,\text{deg}} = n$$$

Lean4

@[simp]
theorem degree_zero : degree (0 : R[T;T⁻¹]) = ⊥ :=
  rfl

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

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

Разделы

Аффилиация

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