degree_T_le — Mathlib

English

In the Laurent polynomial ring R[T; T^{-1}] over a semiring R, the Laurent monomial T^n has degree at most n for every integer n.

Русский

В кольце Лорента R[T; T^{-1}] над полем R каждый моном T^n имеет степень не превышающую n для любого целого n.

LaTeX

$$$\\deg(T^n) \\le n$$$

Lean4

theorem degree_T_le (n : ℤ) : (T n : R[T;T⁻¹]).degree ≤ n :=
  (le_of_eq (by rw [map_one, one_mul])).trans (degree_C_mul_T_le n (1 : R))

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