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.
def
PolynomialModule.polynomialTensorProductLEquivPolynomialModule
(R : Type u_1)
(M : Type u_2)
[CommRing R]
[AddCommGroup M]
[Module 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.