T_pow

Mathlib.Algebra.Polynomial.Laurent

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

English

Raising a monomial to a natural power corresponds to multiplying its exponent: (T(m))^n = T(n m).

Русский

Возведение монома T(m) в натуральную степень задаёт умножение его экспоненты: $T(m)^n = T(n m)$.

LaTeX

$$$(T\\ m)^{\\ n} = T\\ (n \\cdot m)$$$

Lean4

@[simp]
theorem T_pow (m : ℤ) (n : ℕ) : (T m ^ n : R[T;T⁻¹]) = T (n * m) := by rw [T, T, single_pow, one_pow, nsmul_eq_mul]

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

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

Разделы

Аффилиация

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