mk'_one_X_pow

Mathlib.Algebra.Polynomial.Laurent

URI: https://scilib.ai/kg/mathlib#LaurentPolynomial.mk'_one_X_pow

← MathLib Explorer

English

For any n ∈ ℕ, IsLocalization.mk' R[T;T⁻¹] 1 (⟨X^n, n, rfl⟩) = T(-n).

Русский

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

LaTeX

$$$\\mathrm{mk'}(1, \\langle X^n, n, rfl\\rangle) = T^{-n}.$$$

Lean4

theorem mk'_one_X_pow (n : ℕ) :
    IsLocalization.mk' R[T;T⁻¹] 1 (⟨X ^ n, n, rfl⟩ : Submonoid.powers (X : R[X])) = T (-n) := by
  rw [mk'_eq 1 n, toLaurent_one, one_mul]

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

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

Разделы

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

Аффилиация

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