English
There is a ring isomorphism between the polynomial ring R[X] and the monoid algebra R[ℕ], given by toFinsuppIso, with forward map toFinsupp and inverse ofFinsupp.
Русский
Существует кольцевое изоморфизм между полиномиальной кольцом R[X] и моноидовой алгеброй R[ℕ], задаваемый toFinsuppIso; переход вперёд — toFinsupp, обратный переход — ofFinsupp.
LaTeX
$$$R[X] \cong_{\mathrm{ring}} R[\mathbb{N}]$ via \mathrm{toFinsuppIso}$$
Lean4
/-- Ring isomorphism between `R[X]` and `R[ℕ]`. This is just an
implementation detail, but it can be useful to transfer results from `Finsupp` to polynomials. -/
@[simps apply symm_apply]
def toFinsuppIso : R[X] ≃+* R[ℕ] where
toFun := toFinsupp
invFun := ofFinsupp
map_mul' := toFinsupp_mul
map_add' := toFinsupp_add
