PolynomialModule F V ≃ₗ[F[X]] F[X] ⊗[F] V

Stream: Is there code for X?

[Sahan Wijetunga]

Is there a direct theorem for PolynomialModule F V ≃ₗ[F[X]] F[X] ⊗[F] V anywhere in Mathlib?

There's MvPolynomial.scalarRTensor but I just want singlevariable

[Yaël Dillies]

There is docs#polyEquivTensor, which is close