mk'_eq — Mathlib

English

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

Русский

Для 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}.$$$

Lean4

@[simp]
theorem mk'_eq (p : R[X]) (n : ℕ) :
    IsLocalization.mk' R[T;T⁻¹] p (⟨X ^ n, n, rfl⟩ : Submonoid.powers (X : R[X])) = toLaurent p * T (-n) :=
  by
  rw [← IsUnit.mul_left_inj (isUnit_T n), mul_T_assoc, neg_add_cancel, T_zero, mul_one]
  exact mk'_mul_T p n

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