T_add

Mathlib.Algebra.Polynomial.Laurent

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

English

The monomial basis is multiplicative with respect to exponent addition: T(m+n) = T(m) T(n).

Русский

База мономов конвергирует умножением: $T(m+n) = T(m) T(n)$.

LaTeX

$$$T(m + n) = T\\,m * T\\,n$$$

Lean4

theorem T_add (m n : ℤ) : (T (m + n) : R[T;T⁻¹]) = T m * T n := by simp [T, single_mul_single]

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

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

Разделы

Аффилиация

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