Documentation

Mathlib.LinearAlgebra.PiTensorProduct

Tensor product of an indexed family of modules over commutative semirings #

We define the tensor product of an indexed family s : ι → Type* of modules over commutative semirings. We denote this space by ⨂[R] i, s i and define it as FreeAddMonoid (R × ∀ i, s i) quotiented by the appropriate equivalence relation. The treatment follows very closely that of the binary tensor product in LinearAlgebra/TensorProduct.lean.

Main definitions #

Notations #

Implementation notes #

TODO #

Tags #

multilinear, tensor, tensor product

inductive PiTensorProduct.Eqv {ι : Type u_1} (R : Type u_4) [CommSemiring R] (s : ιType u_7) [(i : ι) → AddCommMonoid (s i)] [(i : ι) → Module R (s i)] :
FreeAddMonoid (R × ((i : ι) → s i))FreeAddMonoid (R × ((i : ι) → s i))Prop

The relation on FreeAddMonoid (R × ∀ i, s i) that generates a congruence whose quotient is the tensor product.

Instances For
    def PiTensorProduct {ι : Type u_1} (R : Type u_4) [CommSemiring R] (s : ιType u_7) [(i : ι) → AddCommMonoid (s i)] [(i : ι) → Module R (s i)] :
    Type (max (max u_1 u_4) u_7)

    PiTensorProduct R s with R a commutative semiring and s : ι → Type* is the tensor product of all the s i's. This is denoted by ⨂[R] i, s i.

    Instances For

      notation for tensor product over some indexed type

      Instances For
        instance PiTensorProduct.instAddCommMonoidPiTensorProduct {ι : Type u_1} {R : Type u_4} [CommSemiring R] (s : ιType u_7) [(i : ι) → AddCommMonoid (s i)] [(i : ι) → Module R (s i)] :
        AddCommMonoid (⨂[R] (i : ι), s i)
        instance PiTensorProduct.instInhabitedPiTensorProduct {ι : Type u_1} {R : Type u_4} [CommSemiring R] (s : ιType u_7) [(i : ι) → AddCommMonoid (s i)] [(i : ι) → Module R (s i)] :
        Inhabited (⨂[R] (i : ι), s i)
        def PiTensorProduct.tprodCoeff {ι : Type u_1} (R : Type u_4) [CommSemiring R] {s : ιType u_7} [(i : ι) → AddCommMonoid (s i)] [(i : ι) → Module R (s i)] (r : R) (f : (i : ι) → s i) :
        ⨂[R] (i : ι), s i

        tprodCoeff R r f with r : R and f : ∀ i, s i is the tensor product of the vectors f i over all i : ι, multiplied by the coefficient r. Note that this is meant as an auxiliary definition for this file alone, and that one should use tprod defined below for most purposes.

        Instances For
          theorem PiTensorProduct.zero_tprodCoeff {ι : Type u_1} {R : Type u_4} [CommSemiring R] {s : ιType u_7} [(i : ι) → AddCommMonoid (s i)] [(i : ι) → Module R (s i)] (f : (i : ι) → s i) :
          theorem PiTensorProduct.zero_tprodCoeff' {ι : Type u_1} {R : Type u_4} [CommSemiring R] {s : ιType u_7} [(i : ι) → AddCommMonoid (s i)] [(i : ι) → Module R (s i)] (z : R) (f : (i : ι) → s i) (i : ι) (hf : f i = 0) :
          theorem PiTensorProduct.add_tprodCoeff {ι : Type u_1} {R : Type u_4} [CommSemiring R] {s : ιType u_7} [(i : ι) → AddCommMonoid (s i)] [(i : ι) → Module R (s i)] [DecidableEq ι] (z : R) (f : (i : ι) → s i) (i : ι) (m₁ : s i) (m₂ : s i) :
          theorem PiTensorProduct.add_tprodCoeff' {ι : Type u_1} {R : Type u_4} [CommSemiring R] {s : ιType u_7} [(i : ι) → AddCommMonoid (s i)] [(i : ι) → Module R (s i)] (z₁ : R) (z₂ : R) (f : (i : ι) → s i) :
          theorem PiTensorProduct.smul_tprodCoeff_aux {ι : Type u_1} {R : Type u_4} [CommSemiring R] {s : ιType u_7} [(i : ι) → AddCommMonoid (s i)] [(i : ι) → Module R (s i)] [DecidableEq ι] (z : R) (f : (i : ι) → s i) (i : ι) (r : R) :
          theorem PiTensorProduct.smul_tprodCoeff {ι : Type u_1} {R : Type u_4} [CommSemiring R] {R₁ : Type u_5} {s : ιType u_7} [(i : ι) → AddCommMonoid (s i)] [(i : ι) → Module R (s i)] [DecidableEq ι] (z : R) (f : (i : ι) → s i) (i : ι) (r : R₁) [SMul R₁ R] [IsScalarTower R₁ R R] [SMul R₁ (s i)] [IsScalarTower R₁ R (s i)] :
          def PiTensorProduct.liftAddHom {ι : Type u_1} {R : Type u_4} [CommSemiring R] {s : ιType u_7} [(i : ι) → AddCommMonoid (s i)] [(i : ι) → Module R (s i)] {F : Type u_10} [AddCommMonoid F] (φ : R × ((i : ι) → s i)F) (C0 : ∀ (r : R) (f : (i : ι) → s i) (i : ι), f i = 0φ (r, f) = 0) (C0' : ∀ (f : (i : ι) → s i), φ (0, f) = 0) (C_add : ∀ [inst : DecidableEq ι] (r : R) (f : (i : ι) → s i) (i : ι) (m₁ m₂ : s i), φ (r, Function.update f i m₁) + φ (r, Function.update f i m₂) = φ (r, Function.update f i (m₁ + m₂))) (C_add_scalar : ∀ (r r' : R) (f : (i : ι) → s i), φ (r, f) + φ (r', f) = φ (r + r', f)) (C_smul : ∀ [inst : DecidableEq ι] (r : R) (f : (i : ι) → s i) (i : ι) (r' : R), φ (r, Function.update f i (r' f i)) = φ (r' * r, f)) :
          (⨂[R] (i : ι), s i) →+ F

          Construct an AddMonoidHom from (⨂[R] i, s i) to some space F from a function φ : (R × ∀ i, s i) → F with the appropriate properties.

          Instances For
            theorem PiTensorProduct.induction_on' {ι : Type u_1} {R : Type u_4} [CommSemiring R] {s : ιType u_7} [(i : ι) → AddCommMonoid (s i)] [(i : ι) → Module R (s i)] {C : (⨂[R] (i : ι), s i) → Prop} (z : ⨂[R] (i : ι), s i) (C1 : {r : R} → {f : (i : ι) → s i} → C (PiTensorProduct.tprodCoeff R r f)) (Cp : {x y : ⨂[R] (i : ι), s i} → C xC yC (x + y)) :
            C z
            instance PiTensorProduct.hasSMul' {ι : Type u_1} {R : Type u_4} [CommSemiring R] {R₁ : Type u_5} {s : ιType u_7} [(i : ι) → AddCommMonoid (s i)] [(i : ι) → Module R (s i)] [Monoid R₁] [DistribMulAction R₁ R] [SMulCommClass R₁ R R] :
            SMul R₁ (⨂[R] (i : ι), s i)
            instance PiTensorProduct.instSMulPiTensorProduct {ι : Type u_1} {R : Type u_4} [CommSemiring R] {s : ιType u_7} [(i : ι) → AddCommMonoid (s i)] [(i : ι) → Module R (s i)] :
            SMul R (⨂[R] (i : ι), s i)
            theorem PiTensorProduct.smul_tprodCoeff' {ι : Type u_1} {R : Type u_4} [CommSemiring R] {R₁ : Type u_5} {s : ιType u_7} [(i : ι) → AddCommMonoid (s i)] [(i : ι) → Module R (s i)] [Monoid R₁] [DistribMulAction R₁ R] [SMulCommClass R₁ R R] (r : R₁) (z : R) (f : (i : ι) → s i) :
            theorem PiTensorProduct.smul_add {ι : Type u_1} {R : Type u_4} [CommSemiring R] {R₁ : Type u_5} {s : ιType u_7} [(i : ι) → AddCommMonoid (s i)] [(i : ι) → Module R (s i)] [Monoid R₁] [DistribMulAction R₁ R] [SMulCommClass R₁ R R] (r : R₁) (x : ⨂[R] (i : ι), s i) (y : ⨂[R] (i : ι), s i) :
            r (x + y) = r x + r y
            instance PiTensorProduct.distribMulAction' {ι : Type u_1} {R : Type u_4} [CommSemiring R] {R₁ : Type u_5} {s : ιType u_7} [(i : ι) → AddCommMonoid (s i)] [(i : ι) → Module R (s i)] [Monoid R₁] [DistribMulAction R₁ R] [SMulCommClass R₁ R R] :
            DistribMulAction R₁ (⨂[R] (i : ι), s i)
            instance PiTensorProduct.smulCommClass' {ι : Type u_1} {R : Type u_4} [CommSemiring R] {R₁ : Type u_5} {R₂ : Type u_6} {s : ιType u_7} [(i : ι) → AddCommMonoid (s i)] [(i : ι) → Module R (s i)] [Monoid R₁] [DistribMulAction R₁ R] [SMulCommClass R₁ R R] [Monoid R₂] [DistribMulAction R₂ R] [SMulCommClass R₂ R R] [SMulCommClass R₁ R₂ R] :
            SMulCommClass R₁ R₂ (⨂[R] (i : ι), s i)
            instance PiTensorProduct.isScalarTower' {ι : Type u_1} {R : Type u_4} [CommSemiring R] {R₁ : Type u_5} {R₂ : Type u_6} {s : ιType u_7} [(i : ι) → AddCommMonoid (s i)] [(i : ι) → Module R (s i)] [Monoid R₁] [DistribMulAction R₁ R] [SMulCommClass R₁ R R] [Monoid R₂] [DistribMulAction R₂ R] [SMulCommClass R₂ R R] [SMul R₁ R₂] [IsScalarTower R₁ R₂ R] :
            IsScalarTower R₁ R₂ (⨂[R] (i : ι), s i)
            instance PiTensorProduct.module' {ι : Type u_1} {R : Type u_4} [CommSemiring R] {R₁ : Type u_5} {s : ιType u_7} [(i : ι) → AddCommMonoid (s i)] [(i : ι) → Module R (s i)] [Semiring R₁] [Module R₁ R] [SMulCommClass R₁ R R] :
            Module R₁ (⨂[R] (i : ι), s i)
            instance PiTensorProduct.instModulePiTensorProductToSemiringInstAddCommMonoidPiTensorProduct {ι : Type u_1} {R : Type u_4} [CommSemiring R] {s : ιType u_7} [(i : ι) → AddCommMonoid (s i)] [(i : ι) → Module R (s i)] :
            Module R (⨂[R] (i : ι), s i)
            instance PiTensorProduct.instSMulCommClassPiTensorProductInstSMulPiTensorProduct {ι : Type u_1} {R : Type u_4} [CommSemiring R] {s : ιType u_7} [(i : ι) → AddCommMonoid (s i)] [(i : ι) → Module R (s i)] :
            SMulCommClass R R (⨂[R] (i : ι), s i)
            instance PiTensorProduct.instIsScalarTowerPiTensorProductToSMulToSemiringIdInstSMulPiTensorProduct {ι : Type u_1} {R : Type u_4} [CommSemiring R] {s : ιType u_7} [(i : ι) → AddCommMonoid (s i)] [(i : ι) → Module R (s i)] :
            IsScalarTower R R (⨂[R] (i : ι), s i)
            def PiTensorProduct.tprod {ι : Type u_1} (R : Type u_4) [CommSemiring R] {s : ιType u_7} [(i : ι) → AddCommMonoid (s i)] [(i : ι) → Module R (s i)] :
            MultilinearMap R s (⨂[R] (i : ι), s i)

            The canonical MultilinearMap R s (⨂[R] i, s i).

            Instances For

              pure tensor in tensor product over some index type

              Instances For
                theorem PiTensorProduct.tprod_eq_tprodCoeff_one {ι : Type u_1} {R : Type u_4} [CommSemiring R] {s : ιType u_7} [(i : ι) → AddCommMonoid (s i)] [(i : ι) → Module R (s i)] :
                @[simp]
                theorem PiTensorProduct.tprodCoeff_eq_smul_tprod {ι : Type u_1} {R : Type u_4} [CommSemiring R] {s : ιType u_7} [(i : ι) → AddCommMonoid (s i)] [(i : ι) → Module R (s i)] (z : R) (f : (i : ι) → s i) :
                theorem PiTensorProduct.induction_on {ι : Type u_1} {R : Type u_4} [CommSemiring R] {s : ιType u_7} [(i : ι) → AddCommMonoid (s i)] [(i : ι) → Module R (s i)] {C : (⨂[R] (i : ι), s i) → Prop} (z : ⨂[R] (i : ι), s i) (C1 : {r : R} → {f : (i : ι) → s i} → C (r ↑(PiTensorProduct.tprod R) f)) (Cp : {x y : ⨂[R] (i : ι), s i} → C xC yC (x + y)) :
                C z
                theorem PiTensorProduct.ext {ι : Type u_1} {R : Type u_4} [CommSemiring R] {s : ιType u_7} [(i : ι) → AddCommMonoid (s i)] [(i : ι) → Module R (s i)] {E : Type u_9} [AddCommMonoid E] [Module R E] {φ₁ : (⨂[R] (i : ι), s i) →ₗ[R] E} {φ₂ : (⨂[R] (i : ι), s i) →ₗ[R] E} (H : LinearMap.compMultilinearMap φ₁ (PiTensorProduct.tprod R) = LinearMap.compMultilinearMap φ₂ (PiTensorProduct.tprod R)) :
                φ₁ = φ₂
                def PiTensorProduct.liftAux {ι : Type u_1} {R : Type u_4} [CommSemiring R] {s : ιType u_7} [(i : ι) → AddCommMonoid (s i)] [(i : ι) → Module R (s i)] {E : Type u_9} [AddCommMonoid E] [Module R E] (φ : MultilinearMap R s E) :
                (⨂[R] (i : ι), s i) →+ E

                Auxiliary function to constructing a linear map (⨂[R] i, s i) → E given a MultilinearMap R s E with the property that its composition with the canonical MultilinearMap R s (⨂[R] i, s i) is the given multilinear map.

                Instances For
                  theorem PiTensorProduct.liftAux_tprod {ι : Type u_1} {R : Type u_4} [CommSemiring R] {s : ιType u_7} [(i : ι) → AddCommMonoid (s i)] [(i : ι) → Module R (s i)] {E : Type u_9} [AddCommMonoid E] [Module R E] (φ : MultilinearMap R s E) (f : (i : ι) → s i) :
                  theorem PiTensorProduct.liftAux_tprodCoeff {ι : Type u_1} {R : Type u_4} [CommSemiring R] {s : ιType u_7} [(i : ι) → AddCommMonoid (s i)] [(i : ι) → Module R (s i)] {E : Type u_9} [AddCommMonoid E] [Module R E] (φ : MultilinearMap R s E) (z : R) (f : (i : ι) → s i) :
                  theorem PiTensorProduct.liftAux.smul {ι : Type u_1} {R : Type u_4} [CommSemiring R] {s : ιType u_7} [(i : ι) → AddCommMonoid (s i)] [(i : ι) → Module R (s i)] {E : Type u_9} [AddCommMonoid E] [Module R E] {φ : MultilinearMap R s E} (r : R) (x : ⨂[R] (i : ι), s i) :
                  def PiTensorProduct.lift {ι : Type u_1} {R : Type u_4} [CommSemiring R] {s : ιType u_7} [(i : ι) → AddCommMonoid (s i)] [(i : ι) → Module R (s i)] {E : Type u_9} [AddCommMonoid E] [Module R E] :
                  MultilinearMap R s E ≃ₗ[R] (⨂[R] (i : ι), s i) →ₗ[R] E

                  Constructing a linear map (⨂[R] i, s i) → E given a MultilinearMap R s E with the property that its composition with the canonical MultilinearMap R s E is the given multilinear map φ.

                  Instances For
                    @[simp]
                    theorem PiTensorProduct.lift.tprod {ι : Type u_1} {R : Type u_4} [CommSemiring R] {s : ιType u_7} [(i : ι) → AddCommMonoid (s i)] [(i : ι) → Module R (s i)] {E : Type u_9} [AddCommMonoid E] [Module R E] {φ : MultilinearMap R s E} (f : (i : ι) → s i) :
                    ↑(PiTensorProduct.lift φ) (↑(PiTensorProduct.tprod R) f) = φ f
                    theorem PiTensorProduct.lift.unique' {ι : Type u_1} {R : Type u_4} [CommSemiring R] {s : ιType u_7} [(i : ι) → AddCommMonoid (s i)] [(i : ι) → Module R (s i)] {E : Type u_9} [AddCommMonoid E] [Module R E] {φ : MultilinearMap R s E} {φ' : (⨂[R] (i : ι), s i) →ₗ[R] E} (H : LinearMap.compMultilinearMap φ' (PiTensorProduct.tprod R) = φ) :
                    φ' = PiTensorProduct.lift φ
                    theorem PiTensorProduct.lift.unique {ι : Type u_1} {R : Type u_4} [CommSemiring R] {s : ιType u_7} [(i : ι) → AddCommMonoid (s i)] [(i : ι) → Module R (s i)] {E : Type u_9} [AddCommMonoid E] [Module R E] {φ : MultilinearMap R s E} {φ' : (⨂[R] (i : ι), s i) →ₗ[R] E} (H : ∀ (f : (i : ι) → s i), φ' (↑(PiTensorProduct.tprod R) f) = φ f) :
                    φ' = PiTensorProduct.lift φ
                    @[simp]
                    theorem PiTensorProduct.lift_symm {ι : Type u_1} {R : Type u_4} [CommSemiring R] {s : ιType u_7} [(i : ι) → AddCommMonoid (s i)] [(i : ι) → Module R (s i)] {E : Type u_9} [AddCommMonoid E] [Module R E] (φ' : (⨂[R] (i : ι), s i) →ₗ[R] E) :
                    @[simp]
                    theorem PiTensorProduct.lift_tprod {ι : Type u_1} {R : Type u_4} [CommSemiring R] {s : ιType u_7} [(i : ι) → AddCommMonoid (s i)] [(i : ι) → Module R (s i)] :
                    PiTensorProduct.lift (PiTensorProduct.tprod R) = LinearMap.id
                    def PiTensorProduct.reindex {ι : Type u_1} {ι₂ : Type u_2} (R : Type u_4) [CommSemiring R] (M : Type u_8) [AddCommMonoid M] [Module R M] (e : ι ι₂) :
                    (⨂[R] (x : ι), M) ≃ₗ[R] ⨂[R] (x : ι₂), M

                    Re-index the components of the tensor power by e.

                    For simplicity, this is defined only for homogeneously- (rather than dependently-) typed components.

                    Instances For
                      @[simp]
                      theorem PiTensorProduct.reindex_tprod {ι : Type u_1} {ι₂ : Type u_2} {R : Type u_4} [CommSemiring R] {M : Type u_8} [AddCommMonoid M] [Module R M] (e : ι ι₂) (f : ιM) :
                      ↑(PiTensorProduct.reindex R M e) (↑(PiTensorProduct.tprod R) f) = ⨂ₜ[R] (i : ι₂), f (e.symm i)
                      @[simp]
                      theorem PiTensorProduct.lift_comp_reindex {ι : Type u_1} {ι₂ : Type u_2} {R : Type u_4} [CommSemiring R] {M : Type u_8} [AddCommMonoid M] [Module R M] {E : Type u_9} [AddCommMonoid E] [Module R E] (e : ι ι₂) (φ : MultilinearMap R (fun x => M) E) :
                      LinearMap.comp (PiTensorProduct.lift φ) ↑(PiTensorProduct.reindex R M e) = PiTensorProduct.lift (MultilinearMap.domDomCongr e.symm φ)
                      @[simp]
                      theorem PiTensorProduct.lift_reindex {ι : Type u_1} {ι₂ : Type u_2} {R : Type u_4} [CommSemiring R] {M : Type u_8} [AddCommMonoid M] [Module R M] {E : Type u_9} [AddCommMonoid E] [Module R E] (e : ι ι₂) (φ : MultilinearMap R (fun x => M) E) (x : ⨂[R] (x : ι), M) :
                      ↑(PiTensorProduct.lift φ) (↑(PiTensorProduct.reindex R M e) x) = ↑(PiTensorProduct.lift (MultilinearMap.domDomCongr e.symm φ)) x
                      @[simp]
                      theorem PiTensorProduct.reindex_trans {ι : Type u_1} {ι₂ : Type u_2} {ι₃ : Type u_3} {R : Type u_4} [CommSemiring R] {M : Type u_8} [AddCommMonoid M] [Module R M] (e : ι ι₂) (e' : ι₂ ι₃) :
                      @[simp]
                      theorem PiTensorProduct.reindex_reindex {ι : Type u_1} {ι₂ : Type u_2} {ι₃ : Type u_3} {R : Type u_4} [CommSemiring R] {M : Type u_8} [AddCommMonoid M] [Module R M] (e : ι ι₂) (e' : ι₂ ι₃) (x : ⨂[R] (x : ι), M) :
                      ↑(PiTensorProduct.reindex R M e') (↑(PiTensorProduct.reindex R M e) x) = ↑(PiTensorProduct.reindex R M (e.trans e')) x
                      @[simp]
                      theorem PiTensorProduct.reindex_symm {ι : Type u_1} {ι₂ : Type u_2} {R : Type u_4} [CommSemiring R] {M : Type u_8} [AddCommMonoid M] [Module R M] (e : ι ι₂) :
                      @[simp]
                      theorem PiTensorProduct.reindex_refl {ι : Type u_1} {R : Type u_4} [CommSemiring R] {M : Type u_8} [AddCommMonoid M] [Module R M] :
                      PiTensorProduct.reindex R M (Equiv.refl ι) = LinearEquiv.refl R (⨂[R] (x : ι), M)
                      @[simp]
                      theorem PiTensorProduct.isEmptyEquiv_symm_apply (ι : Type u_1) {R : Type u_4} [CommSemiring R] {M : Type u_8} [AddCommMonoid M] [Module R M] [IsEmpty ι] (r : R) :
                      def PiTensorProduct.isEmptyEquiv (ι : Type u_1) {R : Type u_4} [CommSemiring R] {M : Type u_8} [AddCommMonoid M] [Module R M] [IsEmpty ι] :
                      (⨂[R] (x : ι), M) ≃ₗ[R] R

                      The tensor product over an empty index type ι is isomorphic to the base ring.

                      Instances For
                        @[simp]
                        theorem PiTensorProduct.isEmptyEquiv_apply_tprod (ι : Type u_1) {R : Type u_4} [CommSemiring R] {M : Type u_8} [AddCommMonoid M] [Module R M] [IsEmpty ι] (f : ιM) :
                        @[simp]
                        theorem PiTensorProduct.subsingletonEquiv_symm_apply {ι : Type u_1} {R : Type u_4} [CommSemiring R] {M : Type u_8} [AddCommMonoid M] [Module R M] [Subsingleton ι] (i₀ : ι) (m : M) :
                        ↑(LinearEquiv.symm (PiTensorProduct.subsingletonEquiv i₀)) m = ⨂ₜ[R] (x : ι), m
                        def PiTensorProduct.subsingletonEquiv {ι : Type u_1} {R : Type u_4} [CommSemiring R] {M : Type u_8} [AddCommMonoid M] [Module R M] [Subsingleton ι] (i₀ : ι) :
                        (⨂[R] (x : ι), M) ≃ₗ[R] M

                        Tensor product of M over a singleton set is equivalent to M

                        Instances For
                          @[simp]
                          theorem PiTensorProduct.subsingletonEquiv_apply_tprod {ι : Type u_1} {R : Type u_4} [CommSemiring R] {M : Type u_8} [AddCommMonoid M] [Module R M] [Subsingleton ι] (i : ι) (f : ιM) :
                          def PiTensorProduct.tmulEquiv {ι : Type u_1} {ι₂ : Type u_2} (R : Type u_4) [CommSemiring R] (M : Type u_8) [AddCommMonoid M] [Module R M] :
                          TensorProduct R (⨂[R] (x : ι), M) (⨂[R] (x : ι₂), M) ≃ₗ[R] ⨂[R] (x : ι ι₂), M

                          Equivalence between a TensorProduct of PiTensorProducts and a single PiTensorProduct indexed by a Sum type.

                          For simplicity, this is defined only for homogeneously- (rather than dependently-) typed components.

                          Instances For
                            @[simp]
                            theorem PiTensorProduct.tmulEquiv_apply {ι : Type u_1} {ι₂ : Type u_2} (R : Type u_4) [CommSemiring R] (M : Type u_8) [AddCommMonoid M] [Module R M] (a : ιM) (b : ι₂M) :
                            ↑(PiTensorProduct.tmulEquiv R M) ((⨂ₜ[R] (i : ι), a i) ⊗ₜ[R] ⨂ₜ[R] (i : ι₂), b i) = ⨂ₜ[R] (i : ι ι₂), Sum.elim a b i
                            @[simp]
                            theorem PiTensorProduct.tmulEquiv_symm_apply {ι : Type u_1} {ι₂ : Type u_2} (R : Type u_4) [CommSemiring R] (M : Type u_8) [AddCommMonoid M] [Module R M] (a : ι ι₂M) :
                            ↑(LinearEquiv.symm (PiTensorProduct.tmulEquiv R M)) (⨂ₜ[R] (i : ι ι₂), a i) = (⨂ₜ[R] (i : ι), a (Sum.inl i)) ⊗ₜ[R] ⨂ₜ[R] (i : ι₂), a (Sum.inr i)
                            instance PiTensorProduct.instAddCommGroupPiTensorProductToCommSemiringToAddCommMonoid {ι : Type u_1} {R : Type u_2} [CommRing R] {s : ιType u_3} [(i : ι) → AddCommGroup (s i)] [(i : ι) → Module R (s i)] :
                            AddCommGroup (⨂[R] (i : ι), s i)