invertibleT

Mathlib.Algebra.Polynomial.Laurent

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

← MathLib Explorer

English

For every integer n, T(n) is invertible with inverse T(-n).

Русский

Для каждого целого $n$ моном T(n) имеет обратное $T(-n)$.

LaTeX

$$$\\text{IsUnit}(T(n)) \\\\text{ with inverse } T(-n)$$$

Lean4

instance invertibleT (n : ℤ) : Invertible (T n : R[T;T⁻¹])
    where
  invOf := T (-n)
  invOf_mul_self := by rw [← T_add, neg_add_cancel, T_zero]
  mul_invOf_self := by rw [← T_add, add_neg_cancel, T_zero]

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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