noncomputable def LinearEquiv.chooseBasis_piScalarRight (R : Type u_1) (M : Type u_2) (V : Type u_3) [CommSemiring M] [CommRing R] [Algebra R M] [AddCommGroup V] [Module R V] [Module.Finite R V] [Module.Free R V] : TensorProduct R M V ≃ₗ[M] Module.Free.ChooseBasisIndex R V → M

The M-algebra isomorphism M ⊗ V ≃ₗ[M] (ι → M) coming from the canonical ι-indexed basis of a finite free R-module V.

Equations

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