eval₂_C_mul_T_neg_n

Mathlib.Algebra.Polynomial.Laurent

URI: https://scilib.ai/kg/mathlib#LaurentPolynomial.eval₂_C_mul_T_neg_n

English

For p ∈ R[X] and n ∈ ℕ, IsLocalization.mk' R[T;T⁻¹] p ⟨X^n, n, rfl⟩ · T n = toLaurent p.

Русский

Для p ∈ R[X] и n ∈ ℕ: IsLocalization.mk' p ⟨X^n, n, rfl⟩ · T^n = toLaurent(p).

LaTeX

$$$\\mathrm{mk'}(p, \\langle X^n, n, rfl\\rangle) \\cdot T^{n} = \\mathrm{toLaurent}(p).$$$

Lean4

theorem eval₂_C_mul_T_neg_n (r : R) (n : ℕ) : eval₂ f x (C r * T (-n)) = f r * x⁻¹ ^ n := by
  rw [map_mul, eval₂_T_neg_n, eval₂_C]

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

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

Разделы

Аффилиация

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