ofFinsupp_zero — Mathlib

English

The polynomial corresponding to the zero coefficient function is the zero polynomial: the zero polynomial in R[X] corresponds to ⟨0⟩.

Русский

Полином, соответствующий нулевой функции коэффициентов, есть нулевой полином: нулевой полином в R[X] соответствует ⟨0⟩.

LaTeX

$$$\big(\langle 0 \rangle : R[X]\big) = 0.$$$

Lean4

@[simp]
theorem ofFinsupp_zero : (⟨0⟩ : R[X]) = 0 :=
  rfl

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