equivPolynomial — Mathlib

English

There is an isomorphism between PolynomialModule R S and S[X] as an R-module.

Русский

Существует изоморфизм между PolynomialModule R S и S[X] как R-модуля.

LaTeX

$$PolynomialModule.equivPolynomial : PolynomialModule R S ≃ₗ[R] S[X]$$

Lean4

/-- `PolynomialModule R S` is isomorphic to `S[X]` as an `R` module. -/
noncomputable def equivPolynomial {S : Type*} [CommRing S] [Algebra R S] : PolynomialModule R S ≃ₗ[R] S[X] :=
  { (Polynomial.toFinsuppIso S).symm with map_smul' := fun _ _ => rfl }

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