degree_T — Mathlib

English

The degree of T^n in R[T;T^{-1}] equals n for any integer n, provided R is nontrivial.

Русский

Степень T^n в R[T;T^{-1}] равна n для любого целого n, если R ненулево.

LaTeX

$$$\forall n : \mathbb Z,\ (T^{n} : R[T;T^{-1}]).degree = n$$$

Lean4

@[simp]
theorem degree_T [Nontrivial R] (n : ℤ) : (T n : R[T;T⁻¹]).degree = n :=
  by
  rw [← one_mul (T n), ← map_one C]
  exact degree_C_mul_T n 1 (one_ne_zero : (1 : R) ≠ 0)

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