single_zero_one_eq_one

Mathlib.Algebra.Polynomial.Laurent

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

English

The Laurent polynomial corresponding to a single coefficient at 0 with value 1 is the unit 1.

Русский

Лорантов полином, соответствующий одной единице в нулевой степени, равен единице.

LaTeX

$$$(\\mathsf{single}\\,0\\,1) = 1$$$

Lean4

theorem single_zero_one_eq_one : (Finsupp.single 0 1 : R[T;T⁻¹]) = (1 : R[T;T⁻¹]) :=
  rfl

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

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

Разделы

Аффилиация

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