toFinsupp_ofNat — Mathlib

English

For natural n with AtLeastTwo, the toFinsupp of the nat-embedded polynomial equals the nat-embedded polynomial in R[ℕ].

Русский

Для натурального n с AtLeastTwo отображение toFinsupp константного полинома совпадает с nat-embedded полиномом в R[ℕ].

LaTeX

$$$(\operatorname{ofNat}(n) : R[X]).toFinsupp = \operatorname{ofNat}(n)$$$

Lean4

@[simp]
theorem toFinsupp_ofNat (n : ℕ) [n.AtLeastTwo] : (ofNat(n) : R[X]).toFinsupp = ofNat(n) :=
  rfl

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