eval₂_C_mul_T

Mathlib.Algebra.Polynomial.Laurent

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

English

For any n ∈ ℕ, IsLocalization.mk' R[T;T⁻¹] p ⟨X^n, n, rfl⟩ equals toLaurent(p) · T(-n) for p ∈ R[X].

Русский

Для любого n ∈ ℕ: mk'(p, ⟨X^n, n, rfl⟩) = toLaurent(p) · T(-n).

LaTeX

$$$\\mathrm{mk'}(p, \\langle X^n, n, rfl\\rangle) = \\mathrm{toLaurent}(p) \\cdot T^{-n}$ for all $p\\in R[X], n\\in\\mathbb{N}$.$$

Lean4

@[simp]
theorem eval₂_C_mul_T (r : R) (n : ℤ) : eval₂ f x (C r * T n) = f r * (x ^ n).val := by simp

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

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

Разделы

Аффилиация

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