Theorems · Definition · commutative algebra

Algebra.TensorProduct.basisAux

{R : Type u_1} →
  (A : Type u_2) →
    {M : Type uM} →
      {ι : Type uι} →
        [inst : CommSemiring R] →
          [inst_1 : Semiring A] →
            [inst_2 : Algebra R A] →
              [inst_3 : AddCommMonoid M] → [inst_4 : Module R M] → Module.Basis ι R M → TensorProduct R A M ≃ₗ[R] ι →₀ A

Given an R-algebra A and an R-basis of M, this is an R-linear isomorphism A ⊗[R] M ≃ (ι →₀ A) (which is in fact A-linear).

Defined in

Mathlib.RingTheory.TensorProduct.Free

Cited by

3 results in Mathlib

Foundations

Depth 91 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CommSemiringSemiringAlgebraAddCommMonoidModule