PolynomialModule is isomorphic to a tensor product

For a commutative ring R and an R-module M, we obtain an isomorphism between R[X] ⊗[R] M and PolynomialModule R M as R[X]-modules; this isomorphism is called polynomialTensorProductLEquivPolynomialModule.

noncomputable def PolynomialModule.polynomialTensorProductLEquivPolynomialModule (R : Type u_1) (M : Type u_2) [CommRing R] [AddCommGroup M] [Module R M] : TensorProduct R (Polynomial R) M ≃ₗ[Polynomial R] PolynomialModule R M

The R[X]-linear equivalence (R[X] ⊗[R] M) ≃ₗ[R[X]] (PolynomialModule R M).

Equations

• One or more equations did not get rendered due to their size.