ofFinsupp_erase — Mathlib

English

Casting back from finsupp after erasing the nth coefficient corresponds to erasing the nth coefficient in the polynomial obtained from the finsupp.

Русский

Преобразование из finsupp обратно после стирания n-го коэффициента соответствует удалению n-го коэффициента в многочлене, полученном из finsupp.

LaTeX

$$$\\forall p:\\,AddMonoidAlgebra\ \\,R\ n:\\,\\mathbb{N},\\ (⟨p.erase n⟩ : R[X]) = (⟨p⟩ : R[X]).erase n$$$

Lean4

@[simp]
theorem ofFinsupp_erase (p : R[ℕ]) (n : ℕ) : (⟨p.erase n⟩ : R[X]) = (⟨p⟩ : R[X]).erase n := by simp only [erase_def]

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