mk'_mul_T — Mathlib

English

For a polynomial 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' R[T;T⁻¹] 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 mk'_mul_T (p : R[X]) (n : ℕ) :
    IsLocalization.mk' R[T;T⁻¹] p (⟨X ^ n, n, rfl⟩ : Submonoid.powers (X : R[X])) * T n = toLaurent p := by
  rw [← toLaurent_X_pow, ← algebraMap_eq_toLaurent, IsLocalization.mk'_spec, algebraMap_eq_toLaurent]

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