isUnit_T

Mathlib.Algebra.Polynomial.Laurent

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

English

For every integer n, T(n) is a unit in the Laurent polynomial ring.

Русский

Для каждого целого $n$ моном T(n) является единицей в кольце лаурентовских многочленов.

LaTeX

$$IsUnit( T(n) )$$

Lean4

theorem isUnit_T (n : ℤ) : IsUnit (T n : R[T;T⁻¹]) :=
  isUnit_of_invertible _

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

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

Разделы

Аффилиация

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