eval₂_toLaurent — Mathlib

English

For p ∈ R[X] and n ∈ ℕ, IsLocalization.mk' 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 eval₂_toLaurent (p : R[X]) : eval₂ f x (toLaurent p) = Polynomial.eval₂ f x p :=
  by
  unfold eval₂
  rw [← algebraMap_eq_toLaurent, IsLocalization.lift_eq, coe_eval₂RingHom]

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