Skip to content

Instantly share code, notes, and snippets.

@kbuzzard

kbuzzard/tensorTensorTensorComm.txt Secret

Created September 20, 2023 21:57
Show Gist options
  • Save kbuzzard/4e12434acc12a4ee339f5074f7537958 to your computer and use it in GitHub Desktop.
Save kbuzzard/4e12434acc12a4ee339f5074f7537958 to your computer and use it in GitHub Desktop.
Download ZIP
a massive type
Raw
tensorTensorTensorComm.txt
def TensorProduct.AlgebraTensorModule.tensorTensorTensorComm.{uR, uA, uM, uN, uP, uQ} : (R : Type uR) →
(A : Type uA) →
(M : Type uM) →
(N : Type uN) →
(P : Type uP) →
(Q : Type uQ) →
[inst : CommSemiring.{uR} R] →
[inst_1 : CommSemiring.{uA} A] →
[inst_2 : @Algebra.{uR, uA} R A inst (@CommSemiring.toSemiring.{uA} A inst_1)] →
[inst_3 : AddCommMonoid.{uM} M] →
[inst_4 : @Module.{uR, uM} R M (@CommSemiring.toSemiring.{uR} R inst) inst_3] →
[inst_5 : @Module.{uA, uM} A M (@CommSemiring.toSemiring.{uA} A inst_1) inst_3] →
[inst_6 :
@IsScalarTower.{uM, uA, uR} R A M
(@Algebra.toSMul.{uR, uA} R A inst (@CommSemiring.toSemiring.{uA} A inst_1) inst_2)
(@SMulZeroClass.toSMul.{uM, uA} A M
(@AddMonoid.toZero.{uM} M (@AddCommMonoid.toAddMonoid.{uM} M inst_3))
(@SMulWithZero.toSMulZeroClass.{uM, uA} A M
(@CommMonoidWithZero.toZero.{uA} A (@CommSemiring.toCommMonoidWithZero.{uA} A inst_1))
(@AddMonoid.toZero.{uM} M (@AddCommMonoid.toAddMonoid.{uM} M inst_3))
(@MulActionWithZero.toSMulWithZero.{uM, uA} A M
(@Semiring.toMonoidWithZero.{uA} A (@CommSemiring.toSemiring.{uA} A inst_1))
(@AddMonoid.toZero.{uM} M (@AddCommMonoid.toAddMonoid.{uM} M inst_3))
(@Module.toMulActionWithZero.{uM, uA} A M (@CommSemiring.toSemiring.{uA} A inst_1)
inst_3 inst_5))))
(@SMulZeroClass.toSMul.{uM, uR} R M
(@AddMonoid.toZero.{uM} M (@AddCommMonoid.toAddMonoid.{uM} M inst_3))
(@SMulWithZero.toSMulZeroClass.{uM, uR} R M
(@CommMonoidWithZero.toZero.{uR} R (@CommSemiring.toCommMonoidWithZero.{uR} R inst))
(@AddMonoid.toZero.{uM} M (@AddCommMonoid.toAddMonoid.{uM} M inst_3))
(@MulActionWithZero.toSMulWithZero.{uM, uR} R M
(@Semiring.toMonoidWithZero.{uR} R (@CommSemiring.toSemiring.{uR} R inst))
(@AddMonoid.toZero.{uM} M (@AddCommMonoid.toAddMonoid.{uM} M inst_3))
(@Module.toMulActionWithZero.{uM, uR} R M (@CommSemiring.toSemiring.{uR} R inst)
inst_3 inst_4))))] →
[inst_7 : AddCommMonoid.{uN} N] →
[inst_8 : @Module.{uR, uN} R N (@CommSemiring.toSemiring.{uR} R inst) inst_7] →
[inst_9 : AddCommMonoid.{uP} P] →
[inst_10 : @Module.{uR, uP} R P (@CommSemiring.toSemiring.{uR} R inst) inst_9] →
[inst_11 : @Module.{uA, uP} A P (@CommSemiring.toSemiring.{uA} A inst_1) inst_9] →
[inst_12 :
@IsScalarTower.{uP, uA, uR} R A P
(@Algebra.toSMul.{uR, uA} R A inst (@CommSemiring.toSemiring.{uA} A inst_1)
inst_2)
(@SMulZeroClass.toSMul.{uP, uA} A P
(@AddMonoid.toZero.{uP} P (@AddCommMonoid.toAddMonoid.{uP} P inst_9))
(@SMulWithZero.toSMulZeroClass.{uP, uA} A P
(@CommMonoidWithZero.toZero.{uA} A
(@CommSemiring.toCommMonoidWithZero.{uA} A inst_1))
(@AddMonoid.toZero.{uP} P (@AddCommMonoid.toAddMonoid.{uP} P inst_9))
(@MulActionWithZero.toSMulWithZero.{uP, uA} A P
(@Semiring.toMonoidWithZero.{uA} A
(@CommSemiring.toSemiring.{uA} A inst_1))
(@AddMonoid.toZero.{uP} P (@AddCommMonoid.toAddMonoid.{uP} P inst_9))
(@Module.toMulActionWithZero.{uP, uA} A P
(@CommSemiring.toSemiring.{uA} A inst_1) inst_9 inst_11))))
(@SMulZeroClass.toSMul.{uP, uR} R P
(@AddMonoid.toZero.{uP} P (@AddCommMonoid.toAddMonoid.{uP} P inst_9))
(@SMulWithZero.toSMulZeroClass.{uP, uR} R P
(@CommMonoidWithZero.toZero.{uR} R
(@CommSemiring.toCommMonoidWithZero.{uR} R inst))
(@AddMonoid.toZero.{uP} P (@AddCommMonoid.toAddMonoid.{uP} P inst_9))
(@MulActionWithZero.toSMulWithZero.{uP, uR} R P
(@Semiring.toMonoidWithZero.{uR} R
(@CommSemiring.toSemiring.{uR} R inst))
(@AddMonoid.toZero.{uP} P (@AddCommMonoid.toAddMonoid.{uP} P inst_9))
(@Module.toMulActionWithZero.{uP, uR} R P
(@CommSemiring.toSemiring.{uR} R inst) inst_9 inst_10))))] →
[inst_13 : AddCommMonoid.{uQ} Q] →
[inst_14 :
@Module.{uR, uQ} R Q (@CommSemiring.toSemiring.{uR} R inst) inst_13] →
@LinearEquiv.{max (max uM uP) uN uQ, max (max uM uN) uP uQ, uA, uA} A A
(@CommSemiring.toSemiring.{uA} A inst_1)
(@CommSemiring.toSemiring.{uA} A inst_1)
(@RingHom.id.{uA} A
(@Semiring.toNonAssocSemiring.{uA} A
(@CommSemiring.toSemiring.{uA} A inst_1)))
(@RingHom.id.{uA} A
(@Semiring.toNonAssocSemiring.{uA} A
(@CommSemiring.toSemiring.{uA} A inst_1)))
(@RingHomInvPair.ids.{uA} A (@CommSemiring.toSemiring.{uA} A inst_1))
(@RingHomInvPair.ids.{uA} A (@CommSemiring.toSemiring.{uA} A inst_1))
(@TensorProduct.{max uP uQ, max uM uN, uA} A inst_1
(@TensorProduct.{uN, uM, uR} R inst M N inst_3 inst_7 inst_4 inst_8)
(@TensorProduct.{uQ, uP, uR} R inst P Q inst_9 inst_13 inst_10 inst_14)
(@TensorProduct.addCommMonoid.{uN, uM, uR} R inst M N inst_3 inst_7 inst_4
inst_8)
(@TensorProduct.addCommMonoid.{uQ, uP, uR} R inst P Q inst_9 inst_13
inst_10 inst_14)
(@TensorProduct.leftModule.{uN, uM, uA, uR} R inst A
(@CommSemiring.toSemiring.{uA} A inst_1) M N inst_3 inst_7 inst_4 inst_8
inst_5
(@IsScalarTower.to_smulCommClass.{uM, uA, uR} R inst A
(@CommSemiring.toSemiring.{uA} A inst_1) inst_2 M inst_3 inst_5 inst_4
inst_6))
(@TensorProduct.leftModule.{uQ, uP, uA, uR} R inst A
(@CommSemiring.toSemiring.{uA} A inst_1) P Q inst_9 inst_13 inst_10
inst_14 inst_11
(@IsScalarTower.to_smulCommClass.{uP, uA, uR} R inst A
(@CommSemiring.toSemiring.{uA} A inst_1) inst_2 P inst_9 inst_11
inst_10 inst_12)))
(@TensorProduct.{max uN uQ, max uM uP, uR} R inst
(@TensorProduct.{uP, uM, uA} A inst_1 M P inst_3 inst_9 inst_5 inst_11)
(@TensorProduct.{uQ, uN, uR} R inst N Q inst_7 inst_13 inst_8 inst_14)
(@TensorProduct.addCommMonoid.{uP, uM, uA} A inst_1 M P inst_3 inst_9
inst_5 inst_11)
(@TensorProduct.addCommMonoid.{uQ, uN, uR} R inst N Q inst_7 inst_13
inst_8 inst_14)
(@TensorProduct.leftModule.{uP, uM, uR, uA} A inst_1 R
(@CommSemiring.toSemiring.{uR} R inst) M P inst_3 inst_9 inst_5 inst_11
inst_4
(@IsScalarTower.to_smulCommClass'.{uM, uA, uR} R inst A
(@CommSemiring.toSemiring.{uA} A inst_1) inst_2 M inst_3 inst_5 inst_4
inst_6))
(@TensorProduct.instModuleTensorProductToSemiringAddCommMonoid.{uQ, uN,
uR}
R inst N Q inst_7 inst_13 inst_8 inst_14))
(@TensorProduct.addCommMonoid.{max uP uQ, max uM uN, uA} A inst_1
(@TensorProduct.{uN, uM, uR} R inst M N inst_3 inst_7 inst_4 inst_8)
(@TensorProduct.{uQ, uP, uR} R inst P Q inst_9 inst_13 inst_10 inst_14)
(@TensorProduct.addCommMonoid.{uN, uM, uR} R inst M N inst_3 inst_7 inst_4
inst_8)
(@TensorProduct.addCommMonoid.{uQ, uP, uR} R inst P Q inst_9 inst_13
inst_10 inst_14)
(@TensorProduct.leftModule.{uN, uM, uA, uR} R inst A
(@CommSemiring.toSemiring.{uA} A inst_1) M N inst_3 inst_7 inst_4 inst_8
inst_5
(@IsScalarTower.to_smulCommClass.{uM, uA, uR} R inst A
(@CommSemiring.toSemiring.{uA} A inst_1) inst_2 M inst_3 inst_5 inst_4
inst_6))
(@TensorProduct.leftModule.{uQ, uP, uA, uR} R inst A
(@CommSemiring.toSemiring.{uA} A inst_1) P Q inst_9 inst_13 inst_10
inst_14 inst_11
(@IsScalarTower.to_smulCommClass.{uP, uA, uR} R inst A
(@CommSemiring.toSemiring.{uA} A inst_1) inst_2 P inst_9 inst_11
inst_10 inst_12)))
(@TensorProduct.addCommMonoid.{max uN uQ, max uM uP, uR} R inst
(@TensorProduct.{uP, uM, uA} A inst_1 M P inst_3 inst_9 inst_5 inst_11)
(@TensorProduct.{uQ, uN, uR} R inst N Q inst_7 inst_13 inst_8 inst_14)
(@TensorProduct.addCommMonoid.{uP, uM, uA} A inst_1 M P inst_3 inst_9
inst_5 inst_11)
(@TensorProduct.addCommMonoid.{uQ, uN, uR} R inst N Q inst_7 inst_13
inst_8 inst_14)
(@TensorProduct.leftModule.{uP, uM, uR, uA} A inst_1 R
(@CommSemiring.toSemiring.{uR} R inst) M P inst_3 inst_9 inst_5 inst_11
inst_4
(@IsScalarTower.to_smulCommClass'.{uM, uA, uR} R inst A
(@CommSemiring.toSemiring.{uA} A inst_1) inst_2 M inst_3 inst_5 inst_4
inst_6))
(@TensorProduct.instModuleTensorProductToSemiringAddCommMonoid.{uQ, uN,
uR}
R inst N Q inst_7 inst_13 inst_8 inst_14))
(@TensorProduct.instModuleTensorProductToSemiringAddCommMonoid.{max uP uQ,
max uM uN, uA}
A inst_1
(@TensorProduct.{uN, uM, uR} R inst M N inst_3 inst_7 inst_4 inst_8)
(@TensorProduct.{uQ, uP, uR} R inst P Q inst_9 inst_13 inst_10 inst_14)
(@TensorProduct.addCommMonoid.{uN, uM, uR} R inst M N inst_3 inst_7 inst_4
inst_8)
(@TensorProduct.addCommMonoid.{uQ, uP, uR} R inst P Q inst_9 inst_13
inst_10 inst_14)
(@TensorProduct.leftModule.{uN, uM, uA, uR} R inst A
(@CommSemiring.toSemiring.{uA} A inst_1) M N inst_3 inst_7 inst_4 inst_8
inst_5
(@IsScalarTower.to_smulCommClass.{uM, uA, uR} R inst A
(@CommSemiring.toSemiring.{uA} A inst_1) inst_2 M inst_3 inst_5 inst_4
inst_6))
(@TensorProduct.leftModule.{uQ, uP, uA, uR} R inst A
(@CommSemiring.toSemiring.{uA} A inst_1) P Q inst_9 inst_13 inst_10
inst_14 inst_11
(@IsScalarTower.to_smulCommClass.{uP, uA, uR} R inst A
(@CommSemiring.toSemiring.{uA} A inst_1) inst_2 P inst_9 inst_11
inst_10 inst_12)))
(@TensorProduct.leftModule.{max uN uQ, max uM uP, uA, uR} R inst A
(@CommSemiring.toSemiring.{uA} A inst_1)
(@TensorProduct.{uP, uM, uA} A inst_1 M P inst_3 inst_9 inst_5 inst_11)
(@TensorProduct.{uQ, uN, uR} R inst N Q inst_7 inst_13 inst_8 inst_14)
(@TensorProduct.addCommMonoid.{uP, uM, uA} A inst_1 M P inst_3 inst_9
inst_5 inst_11)
(@TensorProduct.addCommMonoid.{uQ, uN, uR} R inst N Q inst_7 inst_13
inst_8 inst_14)
(@TensorProduct.leftModule.{uP, uM, uR, uA} A inst_1 R
(@CommSemiring.toSemiring.{uR} R inst) M P inst_3 inst_9 inst_5 inst_11
inst_4
(@IsScalarTower.to_smulCommClass'.{uM, uA, uR} R inst A
(@CommSemiring.toSemiring.{uA} A inst_1) inst_2 M inst_3 inst_5 inst_4
inst_6))
(@TensorProduct.instModuleTensorProductToSemiringAddCommMonoid.{uQ, uN,
uR}
R inst N Q inst_7 inst_13 inst_8 inst_14)
(@TensorProduct.instModuleTensorProductToSemiringAddCommMonoid.{uP, uM,
uA}
A inst_1 M P inst_3 inst_9 inst_5 inst_11)
(@TensorProduct.smulCommClass_left.{uA, uP, uM, uR, uA} A inst_1 R
(@MonoidWithZero.toMonoid.{uR} R
(@Semiring.toMonoidWithZero.{uR} R
(@CommSemiring.toSemiring.{uR} R inst)))
M P inst_3 inst_9 inst_5 inst_11
(@Module.toDistribMulAction.{uR, uM} R M
(@CommSemiring.toSemiring.{uR} R inst) inst_3 inst_4)
(@IsScalarTower.to_smulCommClass'.{uM, uA, uR} R inst A
(@CommSemiring.toSemiring.{uA} A inst_1) inst_2 M inst_3 inst_5 inst_4
inst_6)
A
(@MonoidWithZero.toMonoid.{uA} A
(@Semiring.toMonoidWithZero.{uA} A
(@CommSemiring.toSemiring.{uA} A inst_1)))
(@Module.toDistribMulAction.{uA, uM} A M
(@CommSemiring.toSemiring.{uA} A inst_1) inst_3 inst_5)
(@smulCommClass_self.{uM, uA} A M
(@CommSemiring.toCommMonoid.{uA} A inst_1)
(@MulActionWithZero.toMulAction.{uM, uA} A M
(@Semiring.toMonoidWithZero.{uA} A
(@CommSemiring.toSemiring.{uA} A inst_1))
(@AddMonoid.toZero.{uM} M
(@AddCommMonoid.toAddMonoid.{uM} M inst_3))
(@Module.toMulActionWithZero.{uM, uA} A M
(@CommSemiring.toSemiring.{uA} A inst_1) inst_3 inst_5)))
(@IsScalarTower.to_smulCommClass.{uM, uA, uR} R inst A
(@CommSemiring.toSemiring.{uA} A inst_1) inst_2 M inst_3 inst_5 inst_4
inst_6))) :=
fun (R : Type uR) (A : Type uA) (M : Type uM) (N : Type uN) (P : Type uP) (Q : Type uQ) [inst : CommSemiring.{uR} R]
[inst_1 : CommSemiring.{uA} A] [inst_2 : @Algebra.{uR, uA} R A inst (@CommSemiring.toSemiring.{uA} A inst_1)]
[inst_3 : AddCommMonoid.{uM} M] [inst_4 : @Module.{uR, uM} R M (@CommSemiring.toSemiring.{uR} R inst) inst_3]
[inst_5 : @Module.{uA, uM} A M (@CommSemiring.toSemiring.{uA} A inst_1) inst_3]
[inst_6 :
@IsScalarTower.{uM, uA, uR} R A M
(@Algebra.toSMul.{uR, uA} R A inst (@CommSemiring.toSemiring.{uA} A inst_1) inst_2)
(@SMulZeroClass.toSMul.{uM, uA} A M (@AddMonoid.toZero.{uM} M (@AddCommMonoid.toAddMonoid.{uM} M inst_3))
(@SMulWithZero.toSMulZeroClass.{uM, uA} A M
(@CommMonoidWithZero.toZero.{uA} A (@CommSemiring.toCommMonoidWithZero.{uA} A inst_1))
(@AddMonoid.toZero.{uM} M (@AddCommMonoid.toAddMonoid.{uM} M inst_3))
(@MulActionWithZero.toSMulWithZero.{uM, uA} A M
(@Semiring.toMonoidWithZero.{uA} A (@CommSemiring.toSemiring.{uA} A inst_1))
(@AddMonoid.toZero.{uM} M (@AddCommMonoid.toAddMonoid.{uM} M inst_3))
(@Module.toMulActionWithZero.{uM, uA} A M (@CommSemiring.toSemiring.{uA} A inst_1) inst_3 inst_5))))
(@SMulZeroClass.toSMul.{uM, uR} R M (@AddMonoid.toZero.{uM} M (@AddCommMonoid.toAddMonoid.{uM} M inst_3))
(@SMulWithZero.toSMulZeroClass.{uM, uR} R M
(@CommMonoidWithZero.toZero.{uR} R (@CommSemiring.toCommMonoidWithZero.{uR} R inst))
(@AddMonoid.toZero.{uM} M (@AddCommMonoid.toAddMonoid.{uM} M inst_3))
(@MulActionWithZero.toSMulWithZero.{uM, uR} R M
(@Semiring.toMonoidWithZero.{uR} R (@CommSemiring.toSemiring.{uR} R inst))
(@AddMonoid.toZero.{uM} M (@AddCommMonoid.toAddMonoid.{uM} M inst_3))
(@Module.toMulActionWithZero.{uM, uR} R M (@CommSemiring.toSemiring.{uR} R inst) inst_3 inst_4))))]
[inst_7 : AddCommMonoid.{uN} N] [inst_8 : @Module.{uR, uN} R N (@CommSemiring.toSemiring.{uR} R inst) inst_7]
[inst_9 : AddCommMonoid.{uP} P] [inst_10 : @Module.{uR, uP} R P (@CommSemiring.toSemiring.{uR} R inst) inst_9]
[inst_11 : @Module.{uA, uP} A P (@CommSemiring.toSemiring.{uA} A inst_1) inst_9]
[inst_12 :
@IsScalarTower.{uP, uA, uR} R A P
(@Algebra.toSMul.{uR, uA} R A inst (@CommSemiring.toSemiring.{uA} A inst_1) inst_2)
(@SMulZeroClass.toSMul.{uP, uA} A P (@AddMonoid.toZero.{uP} P (@AddCommMonoid.toAddMonoid.{uP} P inst_9))
(@SMulWithZero.toSMulZeroClass.{uP, uA} A P
(@CommMonoidWithZero.toZero.{uA} A (@CommSemiring.toCommMonoidWithZero.{uA} A inst_1))
(@AddMonoid.toZero.{uP} P (@AddCommMonoid.toAddMonoid.{uP} P inst_9))
(@MulActionWithZero.toSMulWithZero.{uP, uA} A P
(@Semiring.toMonoidWithZero.{uA} A (@CommSemiring.toSemiring.{uA} A inst_1))
(@AddMonoid.toZero.{uP} P (@AddCommMonoid.toAddMonoid.{uP} P inst_9))
(@Module.toMulActionWithZero.{uP, uA} A P (@CommSemiring.toSemiring.{uA} A inst_1) inst_9 inst_11))))
(@SMulZeroClass.toSMul.{uP, uR} R P (@AddMonoid.toZero.{uP} P (@AddCommMonoid.toAddMonoid.{uP} P inst_9))
(@SMulWithZero.toSMulZeroClass.{uP, uR} R P
(@CommMonoidWithZero.toZero.{uR} R (@CommSemiring.toCommMonoidWithZero.{uR} R inst))
(@AddMonoid.toZero.{uP} P (@AddCommMonoid.toAddMonoid.{uP} P inst_9))
(@MulActionWithZero.toSMulWithZero.{uP, uR} R P
(@Semiring.toMonoidWithZero.{uR} R (@CommSemiring.toSemiring.{uR} R inst))
(@AddMonoid.toZero.{uP} P (@AddCommMonoid.toAddMonoid.{uP} P inst_9))
(@Module.toMulActionWithZero.{uP, uR} R P (@CommSemiring.toSemiring.{uR} R inst) inst_9 inst_10))))]
[inst_13 : AddCommMonoid.{uQ} Q] [inst_14 : @Module.{uR, uQ} R Q (@CommSemiring.toSemiring.{uR} R inst) inst_13] ↦
@LinearEquiv.trans.{max (max (max uM uN) uP) uQ, max uQ (max uM uN) uP, max (max (max uM uN) uP) uQ, uA, uA, uA} A A A
(@TensorProduct.{max uP uQ, max uM uN, uA} A inst_1
(@TensorProduct.{uN, uM, uR} R inst M N inst_3 inst_7 inst_4 inst_8)
(@TensorProduct.{uQ, uP, uR} R inst P Q inst_9 inst_13 inst_10 inst_14)
(@TensorProduct.addCommMonoid.{uN, uM, uR} R inst M N inst_3 inst_7 inst_4 inst_8)
(@TensorProduct.addCommMonoid.{uQ, uP, uR} R inst P Q inst_9 inst_13 inst_10 inst_14)
(@TensorProduct.leftModule.{uN, uM, uA, uR} R inst A (@CommSemiring.toSemiring.{uA} A inst_1) M N inst_3 inst_7
inst_4 inst_8 inst_5
(@TensorProduct.AlgebraTensorModule.tensorTensorTensorComm.proof_1.{uM, uA, uR} R A M inst inst_1 inst_2 inst_3
inst_4 inst_5 inst_6))
(@TensorProduct.leftModule.{uQ, uP, uA, uR} R inst A (@CommSemiring.toSemiring.{uA} A inst_1) P Q inst_9 inst_13
inst_10 inst_14 inst_11
(@TensorProduct.AlgebraTensorModule.tensorTensorTensorComm.proof_2.{uP, uA, uR} R A P inst inst_1 inst_2 inst_9
inst_10 inst_11 inst_12)))
(@TensorProduct.{uQ, max (max uM uN) uP, uR} R inst
(@TensorProduct.{uN, max uM uP, uR} R inst (@TensorProduct.{uP, uM, uA} A inst_1 M P inst_3 inst_9 inst_5 inst_11)
N (@TensorProduct.addCommMonoid.{uP, uM, uA} A inst_1 M P inst_3 inst_9 inst_5 inst_11) inst_7
(@TensorProduct.leftModule.{uP, uM, uR, uA} A inst_1 R (@CommSemiring.toSemiring.{uR} R inst) M P inst_3 inst_9
inst_5 inst_11 inst_4
(@TensorProduct.AlgebraTensorModule.tensorTensorTensorComm.proof_3.{uM, uR, uA} R A M inst inst_1 inst_2
inst_3 inst_4 inst_5 inst_6))
inst_8)
Q
(@TensorProduct.addCommMonoid.{uN, max uM uP, uR} R inst
(@TensorProduct.{uP, uM, uA} A inst_1 M P inst_3 inst_9 inst_5 inst_11) N
(@TensorProduct.addCommMonoid.{uP, uM, uA} A inst_1 M P inst_3 inst_9 inst_5 inst_11) inst_7
(@TensorProduct.leftModule.{uP, uM, uR, uA} A inst_1 R (@CommSemiring.toSemiring.{uR} R inst) M P inst_3 inst_9
inst_5 inst_11 inst_4
(@TensorProduct.AlgebraTensorModule.tensorTensorTensorComm.proof_3.{uM, uR, uA} R A M inst inst_1 inst_2
inst_3 inst_4 inst_5 inst_6))
inst_8)
inst_13
(@TensorProduct.instModuleTensorProductToSemiringAddCommMonoid.{uN, max uM uP, uR} R inst
(@TensorProduct.{uP, uM, uA} A inst_1 M P inst_3 inst_9 inst_5 inst_11) N
(@TensorProduct.addCommMonoid.{uP, uM, uA} A inst_1 M P inst_3 inst_9 inst_5 inst_11) inst_7
(@TensorProduct.leftModule.{uP, uM, uR, uA} A inst_1 R (@CommSemiring.toSemiring.{uR} R inst) M P inst_3 inst_9
inst_5 inst_11 inst_4
(@TensorProduct.AlgebraTensorModule.tensorTensorTensorComm.proof_3.{uM, uR, uA} R A M inst inst_1 inst_2
inst_3 inst_4 inst_5 inst_6))
inst_8)
inst_14)
(@TensorProduct.{max uN uQ, max uM uP, uR} R inst
(@TensorProduct.{uP, uM, uA} A inst_1 M P inst_3 inst_9 inst_5 inst_11)
(@TensorProduct.{uQ, uN, uR} R inst N Q inst_7 inst_13 inst_8 inst_14)
(@TensorProduct.addCommMonoid.{uP, uM, uA} A inst_1 M P inst_3 inst_9 inst_5 inst_11)
(@TensorProduct.addCommMonoid.{uQ, uN, uR} R inst N Q inst_7 inst_13 inst_8 inst_14)
(@TensorProduct.leftModule.{uP, uM, uR, uA} A inst_1 R (@CommSemiring.toSemiring.{uR} R inst) M P inst_3 inst_9
inst_5 inst_11 inst_4
(@TensorProduct.AlgebraTensorModule.tensorTensorTensorComm.proof_3.{uM, uR, uA} R A M inst inst_1 inst_2 inst_3
inst_4 inst_5 inst_6))
(@TensorProduct.instModuleTensorProductToSemiringAddCommMonoid.{uQ, uN, uR} R inst N Q inst_7 inst_13 inst_8
inst_14))
(@CommSemiring.toSemiring.{uA} A inst_1) (@CommSemiring.toSemiring.{uA} A inst_1)
(@CommSemiring.toSemiring.{uA} A inst_1)
(@TensorProduct.addCommMonoid.{max uP uQ, max uM uN, uA} A inst_1
(@TensorProduct.{uN, uM, uR} R inst M N inst_3 inst_7 inst_4 inst_8)
(@TensorProduct.{uQ, uP, uR} R inst P Q inst_9 inst_13 inst_10 inst_14)
(@TensorProduct.addCommMonoid.{uN, uM, uR} R inst M N inst_3 inst_7 inst_4 inst_8)
(@TensorProduct.addCommMonoid.{uQ, uP, uR} R inst P Q inst_9 inst_13 inst_10 inst_14)
(@TensorProduct.leftModule.{uN, uM, uA, uR} R inst A (@CommSemiring.toSemiring.{uA} A inst_1) M N inst_3 inst_7
inst_4 inst_8 inst_5
(@TensorProduct.AlgebraTensorModule.tensorTensorTensorComm.proof_1.{uM, uA, uR} R A M inst inst_1 inst_2 inst_3
inst_4 inst_5 inst_6))
(@TensorProduct.leftModule.{uQ, uP, uA, uR} R inst A (@CommSemiring.toSemiring.{uA} A inst_1) P Q inst_9 inst_13
inst_10 inst_14 inst_11
(@TensorProduct.AlgebraTensorModule.tensorTensorTensorComm.proof_2.{uP, uA, uR} R A P inst inst_1 inst_2 inst_9
inst_10 inst_11 inst_12)))
(@TensorProduct.addCommMonoid.{uQ, max (max uM uN) uP, uR} R inst
(@TensorProduct.{uN, max uM uP, uR} R inst (@TensorProduct.{uP, uM, uA} A inst_1 M P inst_3 inst_9 inst_5 inst_11)
N (@TensorProduct.addCommMonoid.{uP, uM, uA} A inst_1 M P inst_3 inst_9 inst_5 inst_11) inst_7
(@TensorProduct.leftModule.{uP, uM, uR, uA} A inst_1 R (@CommSemiring.toSemiring.{uR} R inst) M P inst_3 inst_9
inst_5 inst_11 inst_4
(@TensorProduct.AlgebraTensorModule.tensorTensorTensorComm.proof_3.{uM, uR, uA} R A M inst inst_1 inst_2
inst_3 inst_4 inst_5 inst_6))
inst_8)
Q
(@TensorProduct.addCommMonoid.{uN, max uM uP, uR} R inst
(@TensorProduct.{uP, uM, uA} A inst_1 M P inst_3 inst_9 inst_5 inst_11) N
(@TensorProduct.addCommMonoid.{uP, uM, uA} A inst_1 M P inst_3 inst_9 inst_5 inst_11) inst_7
(@TensorProduct.leftModule.{uP, uM, uR, uA} A inst_1 R (@CommSemiring.toSemiring.{uR} R inst) M P inst_3 inst_9
inst_5 inst_11 inst_4
(@TensorProduct.AlgebraTensorModule.tensorTensorTensorComm.proof_3.{uM, uR, uA} R A M inst inst_1 inst_2
inst_3 inst_4 inst_5 inst_6))
inst_8)
inst_13
(@TensorProduct.instModuleTensorProductToSemiringAddCommMonoid.{uN, max uM uP, uR} R inst
(@TensorProduct.{uP, uM, uA} A inst_1 M P inst_3 inst_9 inst_5 inst_11) N
(@TensorProduct.addCommMonoid.{uP, uM, uA} A inst_1 M P inst_3 inst_9 inst_5 inst_11) inst_7
(@TensorProduct.leftModule.{uP, uM, uR, uA} A inst_1 R (@CommSemiring.toSemiring.{uR} R inst) M P inst_3 inst_9
inst_5 inst_11 inst_4
(@TensorProduct.AlgebraTensorModule.tensorTensorTensorComm.proof_3.{uM, uR, uA} R A M inst inst_1 inst_2
inst_3 inst_4 inst_5 inst_6))
inst_8)
inst_14)
(@TensorProduct.addCommMonoid.{max uN uQ, max uM uP, uR} R inst
(@TensorProduct.{uP, uM, uA} A inst_1 M P inst_3 inst_9 inst_5 inst_11)
(@TensorProduct.{uQ, uN, uR} R inst N Q inst_7 inst_13 inst_8 inst_14)
(@TensorProduct.addCommMonoid.{uP, uM, uA} A inst_1 M P inst_3 inst_9 inst_5 inst_11)
(@TensorProduct.addCommMonoid.{uQ, uN, uR} R inst N Q inst_7 inst_13 inst_8 inst_14)
(@TensorProduct.leftModule.{uP, uM, uR, uA} A inst_1 R (@CommSemiring.toSemiring.{uR} R inst) M P inst_3 inst_9
inst_5 inst_11 inst_4
(@TensorProduct.AlgebraTensorModule.tensorTensorTensorComm.proof_3.{uM, uR, uA} R A M inst inst_1 inst_2 inst_3
inst_4 inst_5 inst_6))
(@TensorProduct.instModuleTensorProductToSemiringAddCommMonoid.{uQ, uN, uR} R inst N Q inst_7 inst_13 inst_8
inst_14))
(@TensorProduct.instModuleTensorProductToSemiringAddCommMonoid.{max uP uQ, max uM uN, uA} A inst_1
(@TensorProduct.{uN, uM, uR} R inst M N inst_3 inst_7 inst_4 inst_8)
(@TensorProduct.{uQ, uP, uR} R inst P Q inst_9 inst_13 inst_10 inst_14)
(@TensorProduct.addCommMonoid.{uN, uM, uR} R inst M N inst_3 inst_7 inst_4 inst_8)
(@TensorProduct.addCommMonoid.{uQ, uP, uR} R inst P Q inst_9 inst_13 inst_10 inst_14)
(@TensorProduct.leftModule.{uN, uM, uA, uR} R inst A (@CommSemiring.toSemiring.{uA} A inst_1) M N inst_3 inst_7
inst_4 inst_8 inst_5
(@TensorProduct.AlgebraTensorModule.tensorTensorTensorComm.proof_1.{uM, uA, uR} R A M inst inst_1 inst_2 inst_3
inst_4 inst_5 inst_6))
(@TensorProduct.leftModule.{uQ, uP, uA, uR} R inst A (@CommSemiring.toSemiring.{uA} A inst_1) P Q inst_9 inst_13
inst_10 inst_14 inst_11
(@TensorProduct.AlgebraTensorModule.tensorTensorTensorComm.proof_2.{uP, uA, uR} R A P inst inst_1 inst_2 inst_9
inst_10 inst_11 inst_12)))
(@TensorProduct.leftModule.{uQ, max (max uM uN) uP, uA, uR} R inst A (@CommSemiring.toSemiring.{uA} A inst_1)
(@TensorProduct.{uN, max uM uP, uR} R inst (@TensorProduct.{uP, uM, uA} A inst_1 M P inst_3 inst_9 inst_5 inst_11)
N (@TensorProduct.addCommMonoid.{uP, uM, uA} A inst_1 M P inst_3 inst_9 inst_5 inst_11) inst_7
(@TensorProduct.leftModule.{uP, uM, uR, uA} A inst_1 R (@CommSemiring.toSemiring.{uR} R inst) M P inst_3 inst_9
inst_5 inst_11 inst_4
(@TensorProduct.AlgebraTensorModule.tensorTensorTensorComm.proof_3.{uM, uR, uA} R A M inst inst_1 inst_2
inst_3 inst_4 inst_5 inst_6))
inst_8)
Q
(@TensorProduct.addCommMonoid.{uN, max uM uP, uR} R inst
(@TensorProduct.{uP, uM, uA} A inst_1 M P inst_3 inst_9 inst_5 inst_11) N
(@TensorProduct.addCommMonoid.{uP, uM, uA} A inst_1 M P inst_3 inst_9 inst_5 inst_11) inst_7
(@TensorProduct.leftModule.{uP, uM, uR, uA} A inst_1 R (@CommSemiring.toSemiring.{uR} R inst) M P inst_3 inst_9
inst_5 inst_11 inst_4
(@TensorProduct.AlgebraTensorModule.tensorTensorTensorComm.proof_3.{uM, uR, uA} R A M inst inst_1 inst_2
inst_3 inst_4 inst_5 inst_6))
inst_8)
inst_13
(@TensorProduct.instModuleTensorProductToSemiringAddCommMonoid.{uN, max uM uP, uR} R inst
(@TensorProduct.{uP, uM, uA} A inst_1 M P inst_3 inst_9 inst_5 inst_11) N
(@TensorProduct.addCommMonoid.{uP, uM, uA} A inst_1 M P inst_3 inst_9 inst_5 inst_11) inst_7
(@TensorProduct.leftModule.{uP, uM, uR, uA} A inst_1 R (@CommSemiring.toSemiring.{uR} R inst) M P inst_3 inst_9
inst_5 inst_11 inst_4
(@TensorProduct.AlgebraTensorModule.tensorTensorTensorComm.proof_3.{uM, uR, uA} R A M inst inst_1 inst_2
inst_3 inst_4 inst_5 inst_6))
inst_8)
inst_14
(@TensorProduct.leftModule.{uN, max uM uP, uA, uR} R inst A (@CommSemiring.toSemiring.{uA} A inst_1)
(@TensorProduct.{uP, uM, uA} A inst_1 M P inst_3 inst_9 inst_5 inst_11) N
(@TensorProduct.addCommMonoid.{uP, uM, uA} A inst_1 M P inst_3 inst_9 inst_5 inst_11) inst_7
(@TensorProduct.leftModule.{uP, uM, uR, uA} A inst_1 R (@CommSemiring.toSemiring.{uR} R inst) M P inst_3 inst_9
inst_5 inst_11 inst_4
(@TensorProduct.AlgebraTensorModule.tensorTensorTensorComm.proof_3.{uM, uR, uA} R A M inst inst_1 inst_2
inst_3 inst_4 inst_5 inst_6))
inst_8
(@TensorProduct.instModuleTensorProductToSemiringAddCommMonoid.{uP, uM, uA} A inst_1 M P inst_3 inst_9 inst_5
inst_11)
(@TensorProduct.AlgebraTensorModule.tensorTensorTensorComm.proof_4.{uM, uP, uA, uR} R A M P inst inst_1 inst_2
inst_3 inst_4 inst_5 inst_6 inst_9 inst_11))
(@TensorProduct.AlgebraTensorModule.tensorTensorTensorComm.proof_5.{uM, uN, uP, uA, uR} R A M N P inst inst_1
inst_2 inst_3 inst_4 inst_5 inst_6 inst_7 inst_8 inst_9 inst_11))
(@TensorProduct.leftModule.{max uN uQ, max uM uP, uA, uR} R inst A (@CommSemiring.toSemiring.{uA} A inst_1)
(@TensorProduct.{uP, uM, uA} A inst_1 M P inst_3 inst_9 inst_5 inst_11)
(@TensorProduct.{uQ, uN, uR} R inst N Q inst_7 inst_13 inst_8 inst_14)
(@TensorProduct.addCommMonoid.{uP, uM, uA} A inst_1 M P inst_3 inst_9 inst_5 inst_11)
(@TensorProduct.addCommMonoid.{uQ, uN, uR} R inst N Q inst_7 inst_13 inst_8 inst_14)
(@TensorProduct.leftModule.{uP, uM, uR, uA} A inst_1 R (@CommSemiring.toSemiring.{uR} R inst) M P inst_3 inst_9
inst_5 inst_11 inst_4
(@TensorProduct.AlgebraTensorModule.tensorTensorTensorComm.proof_3.{uM, uR, uA} R A M inst inst_1 inst_2 inst_3
inst_4 inst_5 inst_6))
(@TensorProduct.instModuleTensorProductToSemiringAddCommMonoid.{uQ, uN, uR} R inst N Q inst_7 inst_13 inst_8
inst_14)
(@TensorProduct.instModuleTensorProductToSemiringAddCommMonoid.{uP, uM, uA} A inst_1 M P inst_3 inst_9 inst_5
inst_11)
(@TensorProduct.AlgebraTensorModule.tensorTensorTensorComm.proof_4.{uM, uP, uA, uR} R A M P inst inst_1 inst_2
inst_3 inst_4 inst_5 inst_6 inst_9 inst_11))
(@RingHom.id.{uA} A (@Semiring.toNonAssocSemiring.{uA} A (@CommSemiring.toSemiring.{uA} A inst_1)))
(@RingHom.id.{uA} A (@Semiring.toNonAssocSemiring.{uA} A (@CommSemiring.toSemiring.{uA} A inst_1)))
(@RingHom.id.{uA} A (@Semiring.toNonAssocSemiring.{uA} A (@CommSemiring.toSemiring.{uA} A inst_1)))
(@RingHom.id.{uA} A (@Semiring.toNonAssocSemiring.{uA} A (@CommSemiring.toSemiring.{uA} A inst_1)))
(@RingHom.id.{uA} A (@Semiring.toNonAssocSemiring.{uA} A (@CommSemiring.toSemiring.{uA} A inst_1)))
(@RingHom.id.{uA} A (@Semiring.toNonAssocSemiring.{uA} A (@CommSemiring.toSemiring.{uA} A inst_1)))
(@TensorProduct.AlgebraTensorModule.tensorTensorTensorComm.proof_6.{uA} A inst_1)
(@TensorProduct.AlgebraTensorModule.tensorTensorTensorComm.proof_6.{uA} A inst_1)
(@TensorProduct.AlgebraTensorModule.tensorTensorTensorComm.proof_7.{uA} A inst_1)
(@TensorProduct.AlgebraTensorModule.tensorTensorTensorComm.proof_7.{uA} A inst_1)
(@TensorProduct.AlgebraTensorModule.tensorTensorTensorComm.proof_7.{uA} A inst_1)
(@TensorProduct.AlgebraTensorModule.tensorTensorTensorComm.proof_7.{uA} A inst_1)
(@TensorProduct.AlgebraTensorModule.tensorTensorTensorComm.proof_7.{uA} A inst_1)
(@TensorProduct.AlgebraTensorModule.tensorTensorTensorComm.proof_7.{uA} A inst_1)
(@LinearEquiv.trans.{max uQ (max uM uN) uP, max (max (max uM uN) uP) uQ, max (max (max uM uN) uP) uQ, uA, uA, uA} A
A A
(@TensorProduct.{max uP uQ, max uM uN, uA} A inst_1
(@TensorProduct.{uN, uM, uR} R inst M N inst_3 inst_7 inst_4 inst_8)
(@TensorProduct.{uQ, uP, uR} R inst P Q inst_9 inst_13 inst_10 inst_14)
(@TensorProduct.addCommMonoid.{uN, uM, uR} R inst M N inst_3 inst_7 inst_4 inst_8)
(@TensorProduct.addCommMonoid.{uQ, uP, uR} R inst P Q inst_9 inst_13 inst_10 inst_14)
(@TensorProduct.leftModule.{uN, uM, uA, uR} R inst A (@CommSemiring.toSemiring.{uA} A inst_1) M N inst_3 inst_7
inst_4 inst_8 inst_5
(@TensorProduct.AlgebraTensorModule.tensorTensorTensorComm.proof_1.{uM, uA, uR} R A M inst inst_1 inst_2
inst_3 inst_4 inst_5 inst_6))
(@TensorProduct.leftModule.{uQ, uP, uA, uR} R inst A (@CommSemiring.toSemiring.{uA} A inst_1) P Q inst_9 inst_13
inst_10 inst_14 inst_11
(@TensorProduct.AlgebraTensorModule.tensorTensorTensorComm.proof_2.{uP, uA, uR} R A P inst inst_1 inst_2
inst_9 inst_10 inst_11 inst_12)))
(@TensorProduct.{uQ, max (max uM uN) uP, uR} R inst
(@TensorProduct.{uP, max uM uN, uA} A inst_1
(@TensorProduct.{uN, uM, uR} R inst M N inst_3 inst_7 inst_4 inst_8) P
(@TensorProduct.addCommMonoid.{uN, uM, uR} R inst M N inst_3 inst_7 inst_4 inst_8) inst_9
(@TensorProduct.leftModule.{uN, uM, uA, uR} R inst A (@CommSemiring.toSemiring.{uA} A inst_1) M N inst_3
inst_7 inst_4 inst_8 inst_5
(@TensorProduct.AlgebraTensorModule.tensorTensorTensorComm.proof_1.{uM, uA, uR} R A M inst inst_1 inst_2
inst_3 inst_4 inst_5 inst_6))
inst_11)
Q
(@TensorProduct.addCommMonoid.{uP, max uM uN, uA} A inst_1
(@TensorProduct.{uN, uM, uR} R inst M N inst_3 inst_7 inst_4 inst_8) P
(@TensorProduct.addCommMonoid.{uN, uM, uR} R inst M N inst_3 inst_7 inst_4 inst_8) inst_9
(@TensorProduct.leftModule.{uN, uM, uA, uR} R inst A (@CommSemiring.toSemiring.{uA} A inst_1) M N inst_3
inst_7 inst_4 inst_8 inst_5
(@TensorProduct.AlgebraTensorModule.tensorTensorTensorComm.proof_1.{uM, uA, uR} R A M inst inst_1 inst_2
inst_3 inst_4 inst_5 inst_6))
inst_11)
inst_13
(@TensorProduct.leftModule.{uP, max uM uN, uR, uA} A inst_1 R (@CommSemiring.toSemiring.{uR} R inst)
(@TensorProduct.{uN, uM, uR} R inst M N inst_3 inst_7 inst_4 inst_8) P
(@TensorProduct.addCommMonoid.{uN, uM, uR} R inst M N inst_3 inst_7 inst_4 inst_8) inst_9
(@TensorProduct.leftModule.{uN, uM, uA, uR} R inst A (@CommSemiring.toSemiring.{uA} A inst_1) M N inst_3
inst_7 inst_4 inst_8 inst_5
(@TensorProduct.AlgebraTensorModule.tensorTensorTensorComm.proof_1.{uM, uA, uR} R A M inst inst_1 inst_2
inst_3 inst_4 inst_5 inst_6))
inst_11
(@TensorProduct.instModuleTensorProductToSemiringAddCommMonoid.{uN, uM, uR} R inst M N inst_3 inst_7 inst_4
inst_8)
(@TensorProduct.AlgebraTensorModule.tensorTensorTensorComm.proof_8.{uM, uN, uR, uA} R A M N inst inst_1 inst_2
inst_3 inst_4 inst_5 inst_6 inst_7 inst_8))
inst_14)
(@TensorProduct.{uQ, max (max uM uN) uP, uR} R inst
(@TensorProduct.{uN, max uM uP, uR} R inst
(@TensorProduct.{uP, uM, uA} A inst_1 M P inst_3 inst_9 inst_5 inst_11) N
(@TensorProduct.addCommMonoid.{uP, uM, uA} A inst_1 M P inst_3 inst_9 inst_5 inst_11) inst_7
(@TensorProduct.leftModule.{uP, uM, uR, uA} A inst_1 R (@CommSemiring.toSemiring.{uR} R inst) M P inst_3
inst_9 inst_5 inst_11 inst_4
(@TensorProduct.AlgebraTensorModule.tensorTensorTensorComm.proof_3.{uM, uR, uA} R A M inst inst_1 inst_2
inst_3 inst_4 inst_5 inst_6))
inst_8)
Q
(@TensorProduct.addCommMonoid.{uN, max uM uP, uR} R inst
(@TensorProduct.{uP, uM, uA} A inst_1 M P inst_3 inst_9 inst_5 inst_11) N
(@TensorProduct.addCommMonoid.{uP, uM, uA} A inst_1 M P inst_3 inst_9 inst_5 inst_11) inst_7
(@TensorProduct.leftModule.{uP, uM, uR, uA} A inst_1 R (@CommSemiring.toSemiring.{uR} R inst) M P inst_3
inst_9 inst_5 inst_11 inst_4
(@TensorProduct.AlgebraTensorModule.tensorTensorTensorComm.proof_3.{uM, uR, uA} R A M inst inst_1 inst_2
inst_3 inst_4 inst_5 inst_6))
inst_8)
inst_13
(@TensorProduct.instModuleTensorProductToSemiringAddCommMonoid.{uN, max uM uP, uR} R inst
(@TensorProduct.{uP, uM, uA} A inst_1 M P inst_3 inst_9 inst_5 inst_11) N
(@TensorProduct.addCommMonoid.{uP, uM, uA} A inst_1 M P inst_3 inst_9 inst_5 inst_11) inst_7
(@TensorProduct.leftModule.{uP, uM, uR, uA} A inst_1 R (@CommSemiring.toSemiring.{uR} R inst) M P inst_3
inst_9 inst_5 inst_11 inst_4
(@TensorProduct.AlgebraTensorModule.tensorTensorTensorComm.proof_3.{uM, uR, uA} R A M inst inst_1 inst_2
inst_3 inst_4 inst_5 inst_6))
inst_8)
inst_14)
(@CommSemiring.toSemiring.{uA} A inst_1) (@CommSemiring.toSemiring.{uA} A inst_1)
(@CommSemiring.toSemiring.{uA} A inst_1)
(@TensorProduct.addCommMonoid.{max uP uQ, max uM uN, uA} A inst_1
(@TensorProduct.{uN, uM, uR} R inst M N inst_3 inst_7 inst_4 inst_8)
(@TensorProduct.{uQ, uP, uR} R inst P Q inst_9 inst_13 inst_10 inst_14)
(@TensorProduct.addCommMonoid.{uN, uM, uR} R inst M N inst_3 inst_7 inst_4 inst_8)
(@TensorProduct.addCommMonoid.{uQ, uP, uR} R inst P Q inst_9 inst_13 inst_10 inst_14)
(@TensorProduct.leftModule.{uN, uM, uA, uR} R inst A (@CommSemiring.toSemiring.{uA} A inst_1) M N inst_3 inst_7
inst_4 inst_8 inst_5
(@TensorProduct.AlgebraTensorModule.tensorTensorTensorComm.proof_1.{uM, uA, uR} R A M inst inst_1 inst_2
inst_3 inst_4 inst_5 inst_6))
(@TensorProduct.leftModule.{uQ, uP, uA, uR} R inst A (@CommSemiring.toSemiring.{uA} A inst_1) P Q inst_9 inst_13
inst_10 inst_14 inst_11
(@TensorProduct.AlgebraTensorModule.tensorTensorTensorComm.proof_2.{uP, uA, uR} R A P inst inst_1 inst_2
inst_9 inst_10 inst_11 inst_12)))
(@TensorProduct.addCommMonoid.{uQ, max (max uM uN) uP, uR} R inst
(@TensorProduct.{uP, max uM uN, uA} A inst_1
(@TensorProduct.{uN, uM, uR} R inst M N inst_3 inst_7 inst_4 inst_8) P
(@TensorProduct.addCommMonoid.{uN, uM, uR} R inst M N inst_3 inst_7 inst_4 inst_8) inst_9
(@TensorProduct.leftModule.{uN, uM, uA, uR} R inst A (@CommSemiring.toSemiring.{uA} A inst_1) M N inst_3
inst_7 inst_4 inst_8 inst_5
(@TensorProduct.AlgebraTensorModule.tensorTensorTensorComm.proof_1.{uM, uA, uR} R A M inst inst_1 inst_2
inst_3 inst_4 inst_5 inst_6))
inst_11)
Q
(@TensorProduct.addCommMonoid.{uP, max uM uN, uA} A inst_1
(@TensorProduct.{uN, uM, uR} R inst M N inst_3 inst_7 inst_4 inst_8) P
(@TensorProduct.addCommMonoid.{uN, uM, uR} R inst M N inst_3 inst_7 inst_4 inst_8) inst_9
(@TensorProduct.leftModule.{uN, uM, uA, uR} R inst A (@CommSemiring.toSemiring.{uA} A inst_1) M N inst_3
inst_7 inst_4 inst_8 inst_5
(@TensorProduct.AlgebraTensorModule.tensorTensorTensorComm.proof_1.{uM, uA, uR} R A M inst inst_1 inst_2
inst_3 inst_4 inst_5 inst_6))
inst_11)
inst_13
(@TensorProduct.leftModule.{uP, max uM uN, uR, uA} A inst_1 R (@CommSemiring.toSemiring.{uR} R inst)
(@TensorProduct.{uN, uM, uR} R inst M N inst_3 inst_7 inst_4 inst_8) P
(@TensorProduct.addCommMonoid.{uN, uM, uR} R inst M N inst_3 inst_7 inst_4 inst_8) inst_9
(@TensorProduct.leftModule.{uN, uM, uA, uR} R inst A (@CommSemiring.toSemiring.{uA} A inst_1) M N inst_3
inst_7 inst_4 inst_8 inst_5
(@TensorProduct.AlgebraTensorModule.tensorTensorTensorComm.proof_1.{uM, uA, uR} R A M inst inst_1 inst_2
inst_3 inst_4 inst_5 inst_6))
inst_11
(@TensorProduct.instModuleTensorProductToSemiringAddCommMonoid.{uN, uM, uR} R inst M N inst_3 inst_7 inst_4
inst_8)
(@TensorProduct.AlgebraTensorModule.tensorTensorTensorComm.proof_8.{uM, uN, uR, uA} R A M N inst inst_1 inst_2
inst_3 inst_4 inst_5 inst_6 inst_7 inst_8))
inst_14)
(@TensorProduct.addCommMonoid.{uQ, max (max uM uN) uP, uR} R inst
(@TensorProduct.{uN, max uM uP, uR} R inst
(@TensorProduct.{uP, uM, uA} A inst_1 M P inst_3 inst_9 inst_5 inst_11) N
(@TensorProduct.addCommMonoid.{uP, uM, uA} A inst_1 M P inst_3 inst_9 inst_5 inst_11) inst_7
(@TensorProduct.leftModule.{uP, uM, uR, uA} A inst_1 R (@CommSemiring.toSemiring.{uR} R inst) M P inst_3
inst_9 inst_5 inst_11 inst_4
(@TensorProduct.AlgebraTensorModule.tensorTensorTensorComm.proof_3.{uM, uR, uA} R A M inst inst_1 inst_2
inst_3 inst_4 inst_5 inst_6))
inst_8)
Q
(@TensorProduct.addCommMonoid.{uN, max uM uP, uR} R inst
(@TensorProduct.{uP, uM, uA} A inst_1 M P inst_3 inst_9 inst_5 inst_11) N
(@TensorProduct.addCommMonoid.{uP, uM, uA} A inst_1 M P inst_3 inst_9 inst_5 inst_11) inst_7
(@TensorProduct.leftModule.{uP, uM, uR, uA} A inst_1 R (@CommSemiring.toSemiring.{uR} R inst) M P inst_3
inst_9 inst_5 inst_11 inst_4
(@TensorProduct.AlgebraTensorModule.tensorTensorTensorComm.proof_3.{uM, uR, uA} R A M inst inst_1 inst_2
inst_3 inst_4 inst_5 inst_6))
inst_8)
inst_13
(@TensorProduct.instModuleTensorProductToSemiringAddCommMonoid.{uN, max uM uP, uR} R inst
(@TensorProduct.{uP, uM, uA} A inst_1 M P inst_3 inst_9 inst_5 inst_11) N
(@TensorProduct.addCommMonoid.{uP, uM, uA} A inst_1 M P inst_3 inst_9 inst_5 inst_11) inst_7
(@TensorProduct.leftModule.{uP, uM, uR, uA} A inst_1 R (@CommSemiring.toSemiring.{uR} R inst) M P inst_3
inst_9 inst_5 inst_11 inst_4
(@TensorProduct.AlgebraTensorModule.tensorTensorTensorComm.proof_3.{uM, uR, uA} R A M inst inst_1 inst_2
inst_3 inst_4 inst_5 inst_6))
inst_8)
inst_14)
(@TensorProduct.instModuleTensorProductToSemiringAddCommMonoid.{max uP uQ, max uM uN, uA} A inst_1
(@TensorProduct.{uN, uM, uR} R inst M N inst_3 inst_7 inst_4 inst_8)
(@TensorProduct.{uQ, uP, uR} R inst P Q inst_9 inst_13 inst_10 inst_14)
(@TensorProduct.addCommMonoid.{uN, uM, uR} R inst M N inst_3 inst_7 inst_4 inst_8)
(@TensorProduct.addCommMonoid.{uQ, uP, uR} R inst P Q inst_9 inst_13 inst_10 inst_14)
(@TensorProduct.leftModule.{uN, uM, uA, uR} R inst A (@CommSemiring.toSemiring.{uA} A inst_1) M N inst_3 inst_7
inst_4 inst_8 inst_5
(@TensorProduct.AlgebraTensorModule.tensorTensorTensorComm.proof_1.{uM, uA, uR} R A M inst inst_1 inst_2
inst_3 inst_4 inst_5 inst_6))
(@TensorProduct.leftModule.{uQ, uP, uA, uR} R inst A (@CommSemiring.toSemiring.{uA} A inst_1) P Q inst_9 inst_13
inst_10 inst_14 inst_11
(@TensorProduct.AlgebraTensorModule.tensorTensorTensorComm.proof_2.{uP, uA, uR} R A P inst inst_1 inst_2
inst_9 inst_10 inst_11 inst_12)))
(@TensorProduct.leftModule.{uQ, max (max uM uN) uP, uA, uR} R inst A (@CommSemiring.toSemiring.{uA} A inst_1)
(@TensorProduct.{uP, max uM uN, uA} A inst_1
(@TensorProduct.{uN, uM, uR} R inst M N inst_3 inst_7 inst_4 inst_8) P
(@TensorProduct.addCommMonoid.{uN, uM, uR} R inst M N inst_3 inst_7 inst_4 inst_8) inst_9
(@TensorProduct.leftModule.{uN, uM, uA, uR} R inst A (@CommSemiring.toSemiring.{uA} A inst_1) M N inst_3
inst_7 inst_4 inst_8 inst_5
(@TensorProduct.AlgebraTensorModule.tensorTensorTensorComm.proof_1.{uM, uA, uR} R A M inst inst_1 inst_2
inst_3 inst_4 inst_5 inst_6))
inst_11)
Q
(@TensorProduct.addCommMonoid.{uP, max uM uN, uA} A inst_1
(@TensorProduct.{uN, uM, uR} R inst M N inst_3 inst_7 inst_4 inst_8) P
(@TensorProduct.addCommMonoid.{uN, uM, uR} R inst M N inst_3 inst_7 inst_4 inst_8) inst_9
(@TensorProduct.leftModule.{uN, uM, uA, uR} R inst A (@CommSemiring.toSemiring.{uA} A inst_1) M N inst_3
inst_7 inst_4 inst_8 inst_5
(@TensorProduct.AlgebraTensorModule.tensorTensorTensorComm.proof_1.{uM, uA, uR} R A M inst inst_1 inst_2
inst_3 inst_4 inst_5 inst_6))
inst_11)
inst_13
(@TensorProduct.leftModule.{uP, max uM uN, uR, uA} A inst_1 R (@CommSemiring.toSemiring.{uR} R inst)
(@TensorProduct.{uN, uM, uR} R inst M N inst_3 inst_7 inst_4 inst_8) P
(@TensorProduct.addCommMonoid.{uN, uM, uR} R inst M N inst_3 inst_7 inst_4 inst_8) inst_9
(@TensorProduct.leftModule.{uN, uM, uA, uR} R inst A (@CommSemiring.toSemiring.{uA} A inst_1) M N inst_3
inst_7 inst_4 inst_8 inst_5
(@TensorProduct.AlgebraTensorModule.tensorTensorTensorComm.proof_1.{uM, uA, uR} R A M inst inst_1 inst_2
inst_3 inst_4 inst_5 inst_6))
inst_11
(@TensorProduct.instModuleTensorProductToSemiringAddCommMonoid.{uN, uM, uR} R inst M N inst_3 inst_7 inst_4
inst_8)
(@TensorProduct.AlgebraTensorModule.tensorTensorTensorComm.proof_8.{uM, uN, uR, uA} R A M N inst inst_1 inst_2
inst_3 inst_4 inst_5 inst_6 inst_7 inst_8))
inst_14
(@TensorProduct.leftModule.{uP, max uM uN, uA, uA} A inst_1 A (@CommSemiring.toSemiring.{uA} A inst_1)
(@TensorProduct.{uN, uM, uR} R inst M N inst_3 inst_7 inst_4 inst_8) P
(@TensorProduct.addCommMonoid.{uN, uM, uR} R inst M N inst_3 inst_7 inst_4 inst_8) inst_9
(@TensorProduct.leftModule.{uN, uM, uA, uR} R inst A (@CommSemiring.toSemiring.{uA} A inst_1) M N inst_3
inst_7 inst_4 inst_8 inst_5
(@TensorProduct.AlgebraTensorModule.tensorTensorTensorComm.proof_1.{uM, uA, uR} R A M inst inst_1 inst_2
inst_3 inst_4 inst_5 inst_6))
inst_11
(@TensorProduct.leftModule.{uN, uM, uA, uR} R inst A (@CommSemiring.toSemiring.{uA} A inst_1) M N inst_3
inst_7 inst_4 inst_8 inst_5
(@TensorProduct.AlgebraTensorModule.tensorTensorTensorComm.proof_1.{uM, uA, uR} R A M inst inst_1 inst_2
inst_3 inst_4 inst_5 inst_6))
(@TensorProduct.AlgebraTensorModule.tensorTensorTensorComm.proof_9.{uM, uN, uA, uR} R A M N inst inst_1 inst_2
inst_3 inst_4 inst_5 inst_6 inst_7 inst_8))
(@TensorProduct.AlgebraTensorModule.tensorTensorTensorComm.proof_10.{uM, uN, uP, uA, uR} R A M N P inst inst_1
inst_2 inst_3 inst_4 inst_5 inst_6 inst_7 inst_8 inst_9 inst_11))
(@TensorProduct.leftModule.{uQ, max (max uM uN) uP, uA, uR} R inst A (@CommSemiring.toSemiring.{uA} A inst_1)
(@TensorProduct.{uN, max uM uP, uR} R inst
(@TensorProduct.{uP, uM, uA} A inst_1 M P inst_3 inst_9 inst_5 inst_11) N
(@TensorProduct.addCommMonoid.{uP, uM, uA} A inst_1 M P inst_3 inst_9 inst_5 inst_11) inst_7
(@TensorProduct.leftModule.{uP, uM, uR, uA} A inst_1 R (@CommSemiring.toSemiring.{uR} R inst) M P inst_3
inst_9 inst_5 inst_11 inst_4
(@TensorProduct.AlgebraTensorModule.tensorTensorTensorComm.proof_3.{uM, uR, uA} R A M inst inst_1 inst_2
inst_3 inst_4 inst_5 inst_6))
inst_8)
Q
(@TensorProduct.addCommMonoid.{uN, max uM uP, uR} R inst
(@TensorProduct.{uP, uM, uA} A inst_1 M P inst_3 inst_9 inst_5 inst_11) N
(@TensorProduct.addCommMonoid.{uP, uM, uA} A inst_1 M P inst_3 inst_9 inst_5 inst_11) inst_7
(@TensorProduct.leftModule.{uP, uM, uR, uA} A inst_1 R (@CommSemiring.toSemiring.{uR} R inst) M P inst_3
inst_9 inst_5 inst_11 inst_4
(@TensorProduct.AlgebraTensorModule.tensorTensorTensorComm.proof_3.{uM, uR, uA} R A M inst inst_1 inst_2
inst_3 inst_4 inst_5 inst_6))
inst_8)
inst_13
(@TensorProduct.instModuleTensorProductToSemiringAddCommMonoid.{uN, max uM uP, uR} R inst
(@TensorProduct.{uP, uM, uA} A inst_1 M P inst_3 inst_9 inst_5 inst_11) N
(@TensorProduct.addCommMonoid.{uP, uM, uA} A inst_1 M P inst_3 inst_9 inst_5 inst_11) inst_7
(@TensorProduct.leftModule.{uP, uM, uR, uA} A inst_1 R (@CommSemiring.toSemiring.{uR} R inst) M P inst_3
inst_9 inst_5 inst_11 inst_4
(@TensorProduct.AlgebraTensorModule.tensorTensorTensorComm.proof_3.{uM, uR, uA} R A M inst inst_1 inst_2
inst_3 inst_4 inst_5 inst_6))
inst_8)
inst_14
(@TensorProduct.leftModule.{uN, max uM uP, uA, uR} R inst A (@CommSemiring.toSemiring.{uA} A inst_1)
(@TensorProduct.{uP, uM, uA} A inst_1 M P inst_3 inst_9 inst_5 inst_11) N
(@TensorProduct.addCommMonoid.{uP, uM, uA} A inst_1 M P inst_3 inst_9 inst_5 inst_11) inst_7
(@TensorProduct.leftModule.{uP, uM, uR, uA} A inst_1 R (@CommSemiring.toSemiring.{uR} R inst) M P inst_3
inst_9 inst_5 inst_11 inst_4
(@TensorProduct.AlgebraTensorModule.tensorTensorTensorComm.proof_3.{uM, uR, uA} R A M inst inst_1 inst_2
inst_3 inst_4 inst_5 inst_6))
inst_8
(@TensorProduct.instModuleTensorProductToSemiringAddCommMonoid.{uP, uM, uA} A inst_1 M P inst_3 inst_9 inst_5
inst_11)
(@TensorProduct.AlgebraTensorModule.tensorTensorTensorComm.proof_4.{uM, uP, uA, uR} R A M P inst inst_1 inst_2
inst_3 inst_4 inst_5 inst_6 inst_9 inst_11))
(@TensorProduct.AlgebraTensorModule.tensorTensorTensorComm.proof_5.{uM, uN, uP, uA, uR} R A M N P inst inst_1
inst_2 inst_3 inst_4 inst_5 inst_6 inst_7 inst_8 inst_9 inst_11))
(@RingHom.id.{uA} A (@Semiring.toNonAssocSemiring.{uA} A (@CommSemiring.toSemiring.{uA} A inst_1)))
(@RingHom.id.{uA} A (@Semiring.toNonAssocSemiring.{uA} A (@CommSemiring.toSemiring.{uA} A inst_1)))
(@RingHom.id.{uA} A (@Semiring.toNonAssocSemiring.{uA} A (@CommSemiring.toSemiring.{uA} A inst_1)))
(@RingHom.id.{uA} A (@Semiring.toNonAssocSemiring.{uA} A (@CommSemiring.toSemiring.{uA} A inst_1)))
(@RingHom.id.{uA} A (@Semiring.toNonAssocSemiring.{uA} A (@CommSemiring.toSemiring.{uA} A inst_1)))
(@RingHom.id.{uA} A (@Semiring.toNonAssocSemiring.{uA} A (@CommSemiring.toSemiring.{uA} A inst_1)))
(@TensorProduct.AlgebraTensorModule.tensorTensorTensorComm.proof_6.{uA} A inst_1)
(@TensorProduct.AlgebraTensorModule.tensorTensorTensorComm.proof_6.{uA} A inst_1)
(@TensorProduct.AlgebraTensorModule.tensorTensorTensorComm.proof_7.{uA} A inst_1)
(@TensorProduct.AlgebraTensorModule.tensorTensorTensorComm.proof_7.{uA} A inst_1)
(@TensorProduct.AlgebraTensorModule.tensorTensorTensorComm.proof_7.{uA} A inst_1)
(@TensorProduct.AlgebraTensorModule.tensorTensorTensorComm.proof_7.{uA} A inst_1)
(@TensorProduct.AlgebraTensorModule.tensorTensorTensorComm.proof_7.{uA} A inst_1)
(@TensorProduct.AlgebraTensorModule.tensorTensorTensorComm.proof_7.{uA} A inst_1)
(@LinearEquiv.symm.{max (max (max uM uN) uP) uQ, max (max (max uM uN) uP) uQ, uA, uA} A A
(@TensorProduct.{uQ, max (max uM uN) uP, uR} R inst
(@TensorProduct.{uP, max uM uN, uA} A inst_1
(@TensorProduct.{uN, uM, uR} R inst M N inst_3 inst_7 inst_4 inst_8) P
(@TensorProduct.addCommMonoid.{uN, uM, uR} R inst M N inst_3 inst_7 inst_4 inst_8) inst_9
(@TensorProduct.leftModule.{uN, uM, uA, uR} R inst A (@CommSemiring.toSemiring.{uA} A inst_1) M N inst_3
inst_7 inst_4 inst_8 inst_5
(@TensorProduct.AlgebraTensorModule.tensorTensorTensorComm.proof_1.{uM, uA, uR} R A M inst inst_1 inst_2
inst_3 inst_4 inst_5 inst_6))
inst_11)
Q
(@TensorProduct.addCommMonoid.{uP, max uM uN, uA} A inst_1
(@TensorProduct.{uN, uM, uR} R inst M N inst_3 inst_7 inst_4 inst_8) P
(@TensorProduct.addCommMonoid.{uN, uM, uR} R inst M N inst_3 inst_7 inst_4 inst_8) inst_9
(@TensorProduct.leftModule.{uN, uM, uA, uR} R inst A (@CommSemiring.toSemiring.{uA} A inst_1) M N inst_3
inst_7 inst_4 inst_8 inst_5
(@TensorProduct.AlgebraTensorModule.tensorTensorTensorComm.proof_1.{uM, uA, uR} R A M inst inst_1 inst_2
inst_3 inst_4 inst_5 inst_6))
inst_11)
inst_13
(@TensorProduct.leftModule.{uP, max uM uN, uR, uA} A inst_1 R (@CommSemiring.toSemiring.{uR} R inst)
(@TensorProduct.{uN, uM, uR} R inst M N inst_3 inst_7 inst_4 inst_8) P
(@TensorProduct.addCommMonoid.{uN, uM, uR} R inst M N inst_3 inst_7 inst_4 inst_8) inst_9
(@TensorProduct.leftModule.{uN, uM, uA, uR} R inst A (@CommSemiring.toSemiring.{uA} A inst_1) M N inst_3
inst_7 inst_4 inst_8 inst_5
(@TensorProduct.AlgebraTensorModule.tensorTensorTensorComm.proof_1.{uM, uA, uR} R A M inst inst_1 inst_2
inst_3 inst_4 inst_5 inst_6))
inst_11
(@TensorProduct.instModuleTensorProductToSemiringAddCommMonoid.{uN, uM, uR} R inst M N inst_3 inst_7 inst_4
inst_8)
(@TensorProduct.AlgebraTensorModule.tensorTensorTensorComm.proof_8.{uM, uN, uR, uA} R A M N inst inst_1
inst_2 inst_3 inst_4 inst_5 inst_6 inst_7 inst_8))
inst_14)
(@TensorProduct.{max uP uQ, max uM uN, uA} A inst_1
(@TensorProduct.{uN, uM, uR} R inst M N inst_3 inst_7 inst_4 inst_8)
(@TensorProduct.{uQ, uP, uR} R inst P Q inst_9 inst_13 inst_10 inst_14)
(@TensorProduct.addCommMonoid.{uN, uM, uR} R inst M N inst_3 inst_7 inst_4 inst_8)
(@TensorProduct.addCommMonoid.{uQ, uP, uR} R inst P Q inst_9 inst_13 inst_10 inst_14)
(@TensorProduct.leftModule.{uN, uM, uA, uR} R inst A (@CommSemiring.toSemiring.{uA} A inst_1) M N inst_3
inst_7 inst_4 inst_8 inst_5
(@TensorProduct.AlgebraTensorModule.tensorTensorTensorComm.proof_1.{uM, uA, uR} R A M inst inst_1 inst_2
inst_3 inst_4 inst_5 inst_6))
(@TensorProduct.leftModule.{uQ, uP, uA, uR} R inst A (@CommSemiring.toSemiring.{uA} A inst_1) P Q inst_9
inst_13 inst_10 inst_14 inst_11
(@TensorProduct.AlgebraTensorModule.tensorTensorTensorComm.proof_2.{uP, uA, uR} R A P inst inst_1 inst_2
inst_9 inst_10 inst_11 inst_12)))
(@CommSemiring.toSemiring.{uA} A inst_1) (@CommSemiring.toSemiring.{uA} A inst_1)
(@TensorProduct.addCommMonoid.{uQ, max (max uM uN) uP, uR} R inst
(@TensorProduct.{uP, max uM uN, uA} A inst_1
(@TensorProduct.{uN, uM, uR} R inst M N inst_3 inst_7 inst_4 inst_8) P
(@TensorProduct.addCommMonoid.{uN, uM, uR} R inst M N inst_3 inst_7 inst_4 inst_8) inst_9
(@TensorProduct.leftModule.{uN, uM, uA, uR} R inst A (@CommSemiring.toSemiring.{uA} A inst_1) M N inst_3
inst_7 inst_4 inst_8 inst_5
(@TensorProduct.AlgebraTensorModule.tensorTensorTensorComm.proof_1.{uM, uA, uR} R A M inst inst_1 inst_2
inst_3 inst_4 inst_5 inst_6))
inst_11)
Q
(@TensorProduct.addCommMonoid.{uP, max uM uN, uA} A inst_1
(@TensorProduct.{uN, uM, uR} R inst M N inst_3 inst_7 inst_4 inst_8) P
(@TensorProduct.addCommMonoid.{uN, uM, uR} R inst M N inst_3 inst_7 inst_4 inst_8) inst_9
(@TensorProduct.leftModule.{uN, uM, uA, uR} R inst A (@CommSemiring.toSemiring.{uA} A inst_1) M N inst_3
inst_7 inst_4 inst_8 inst_5
(@TensorProduct.AlgebraTensorModule.tensorTensorTensorComm.proof_1.{uM, uA, uR} R A M inst inst_1 inst_2
inst_3 inst_4 inst_5 inst_6))
inst_11)
inst_13
(@TensorProduct.leftModule.{uP, max uM uN, uR, uA} A inst_1 R (@CommSemiring.toSemiring.{uR} R inst)
(@TensorProduct.{uN, uM, uR} R inst M N inst_3 inst_7 inst_4 inst_8) P
(@TensorProduct.addCommMonoid.{uN, uM, uR} R inst M N inst_3 inst_7 inst_4 inst_8) inst_9
(@TensorProduct.leftModule.{uN, uM, uA, uR} R inst A (@CommSemiring.toSemiring.{uA} A inst_1) M N inst_3
inst_7 inst_4 inst_8 inst_5
(@TensorProduct.AlgebraTensorModule.tensorTensorTensorComm.proof_1.{uM, uA, uR} R A M inst inst_1 inst_2
inst_3 inst_4 inst_5 inst_6))
inst_11
(@TensorProduct.instModuleTensorProductToSemiringAddCommMonoid.{uN, uM, uR} R inst M N inst_3 inst_7 inst_4
inst_8)
(@TensorProduct.AlgebraTensorModule.tensorTensorTensorComm.proof_8.{uM, uN, uR, uA} R A M N inst inst_1
inst_2 inst_3 inst_4 inst_5 inst_6 inst_7 inst_8))
inst_14)
(@TensorProduct.addCommMonoid.{max uP uQ, max uM uN, uA} A inst_1
(@TensorProduct.{uN, uM, uR} R inst M N inst_3 inst_7 inst_4 inst_8)
(@TensorProduct.{uQ, uP, uR} R inst P Q inst_9 inst_13 inst_10 inst_14)
(@TensorProduct.addCommMonoid.{uN, uM, uR} R inst M N inst_3 inst_7 inst_4 inst_8)
(@TensorProduct.addCommMonoid.{uQ, uP, uR} R inst P Q inst_9 inst_13 inst_10 inst_14)
(@TensorProduct.leftModule.{uN, uM, uA, uR} R inst A (@CommSemiring.toSemiring.{uA} A inst_1) M N inst_3
inst_7 inst_4 inst_8 inst_5
(@TensorProduct.AlgebraTensorModule.tensorTensorTensorComm.proof_1.{uM, uA, uR} R A M inst inst_1 inst_2
inst_3 inst_4 inst_5 inst_6))
(@TensorProduct.leftModule.{uQ, uP, uA, uR} R inst A (@CommSemiring.toSemiring.{uA} A inst_1) P Q inst_9
inst_13 inst_10 inst_14 inst_11
(@TensorProduct.AlgebraTensorModule.tensorTensorTensorComm.proof_2.{uP, uA, uR} R A P inst inst_1 inst_2
inst_9 inst_10 inst_11 inst_12)))
(@TensorProduct.leftModule.{uQ, max (max uM uN) uP, uA, uR} R inst A (@CommSemiring.toSemiring.{uA} A inst_1)
(@TensorProduct.{uP, max uM uN, uA} A inst_1
(@TensorProduct.{uN, uM, uR} R inst M N inst_3 inst_7 inst_4 inst_8) P
(@TensorProduct.addCommMonoid.{uN, uM, uR} R inst M N inst_3 inst_7 inst_4 inst_8) inst_9
(@TensorProduct.leftModule.{uN, uM, uA, uR} R inst A (@CommSemiring.toSemiring.{uA} A inst_1) M N inst_3
inst_7 inst_4 inst_8 inst_5
(@TensorProduct.AlgebraTensorModule.tensorTensorTensorComm.proof_1.{uM, uA, uR} R A M inst inst_1 inst_2
inst_3 inst_4 inst_5 inst_6))
inst_11)
Q
(@TensorProduct.addCommMonoid.{uP, max uM uN, uA} A inst_1
(@TensorProduct.{uN, uM, uR} R inst M N inst_3 inst_7 inst_4 inst_8) P
(@TensorProduct.addCommMonoid.{uN, uM, uR} R inst M N inst_3 inst_7 inst_4 inst_8) inst_9
(@TensorProduct.leftModule.{uN, uM, uA, uR} R inst A (@CommSemiring.toSemiring.{uA} A inst_1) M N inst_3
inst_7 inst_4 inst_8 inst_5
(@TensorProduct.AlgebraTensorModule.tensorTensorTensorComm.proof_1.{uM, uA, uR} R A M inst inst_1 inst_2
inst_3 inst_4 inst_5 inst_6))
inst_11)
inst_13
(@TensorProduct.leftModule.{uP, max uM uN, uR, uA} A inst_1 R (@CommSemiring.toSemiring.{uR} R inst)
(@TensorProduct.{uN, uM, uR} R inst M N inst_3 inst_7 inst_4 inst_8) P
(@TensorProduct.addCommMonoid.{uN, uM, uR} R inst M N inst_3 inst_7 inst_4 inst_8) inst_9
(@TensorProduct.leftModule.{uN, uM, uA, uR} R inst A (@CommSemiring.toSemiring.{uA} A inst_1) M N inst_3
inst_7 inst_4 inst_8 inst_5
(@TensorProduct.AlgebraTensorModule.tensorTensorTensorComm.proof_1.{uM, uA, uR} R A M inst inst_1 inst_2
inst_3 inst_4 inst_5 inst_6))
inst_11
(@TensorProduct.instModuleTensorProductToSemiringAddCommMonoid.{uN, uM, uR} R inst M N inst_3 inst_7 inst_4
inst_8)
(@TensorProduct.AlgebraTensorModule.tensorTensorTensorComm.proof_8.{uM, uN, uR, uA} R A M N inst inst_1
inst_2 inst_3 inst_4 inst_5 inst_6 inst_7 inst_8))
inst_14
(@TensorProduct.leftModule.{uP, max uM uN, uA, uA} A inst_1 A (@CommSemiring.toSemiring.{uA} A inst_1)
(@TensorProduct.{uN, uM, uR} R inst M N inst_3 inst_7 inst_4 inst_8) P
(@TensorProduct.addCommMonoid.{uN, uM, uR} R inst M N inst_3 inst_7 inst_4 inst_8) inst_9
(@TensorProduct.leftModule.{uN, uM, uA, uR} R inst A (@CommSemiring.toSemiring.{uA} A inst_1) M N inst_3
inst_7 inst_4 inst_8 inst_5
(@TensorProduct.AlgebraTensorModule.tensorTensorTensorComm.proof_1.{uM, uA, uR} R A M inst inst_1 inst_2
inst_3 inst_4 inst_5 inst_6))
inst_11
(@TensorProduct.leftModule.{uN, uM, uA, uR} R inst A (@CommSemiring.toSemiring.{uA} A inst_1) M N inst_3
inst_7 inst_4 inst_8 inst_5
(@TensorProduct.AlgebraTensorModule.tensorTensorTensorComm.proof_1.{uM, uA, uR} R A M inst inst_1 inst_2
inst_3 inst_4 inst_5 inst_6))
(@TensorProduct.AlgebraTensorModule.tensorTensorTensorComm.proof_9.{uM, uN, uA, uR} R A M N inst inst_1
inst_2 inst_3 inst_4 inst_5 inst_6 inst_7 inst_8))
(@TensorProduct.AlgebraTensorModule.tensorTensorTensorComm.proof_10.{uM, uN, uP, uA, uR} R A M N P inst inst_1
inst_2 inst_3 inst_4 inst_5 inst_6 inst_7 inst_8 inst_9 inst_11))
(@TensorProduct.leftModule.{max uP uQ, max uM uN, uA, uA} A inst_1 A (@CommSemiring.toSemiring.{uA} A inst_1)
(@TensorProduct.{uN, uM, uR} R inst M N inst_3 inst_7 inst_4 inst_8)
(@TensorProduct.{uQ, uP, uR} R inst P Q inst_9 inst_13 inst_10 inst_14)
(@TensorProduct.addCommMonoid.{uN, uM, uR} R inst M N inst_3 inst_7 inst_4 inst_8)
(@TensorProduct.addCommMonoid.{uQ, uP, uR} R inst P Q inst_9 inst_13 inst_10 inst_14)
(@TensorProduct.leftModule.{uN, uM, uA, uR} R inst A (@CommSemiring.toSemiring.{uA} A inst_1) M N inst_3
inst_7 inst_4 inst_8 inst_5
(@TensorProduct.AlgebraTensorModule.tensorTensorTensorComm.proof_1.{uM, uA, uR} R A M inst inst_1 inst_2
inst_3 inst_4 inst_5 inst_6))
(@TensorProduct.leftModule.{uQ, uP, uA, uR} R inst A (@CommSemiring.toSemiring.{uA} A inst_1) P Q inst_9
inst_13 inst_10 inst_14 inst_11
(@TensorProduct.AlgebraTensorModule.tensorTensorTensorComm.proof_2.{uP, uA, uR} R A P inst inst_1 inst_2
inst_9 inst_10 inst_11 inst_12))
(@TensorProduct.leftModule.{uN, uM, uA, uR} R inst A (@CommSemiring.toSemiring.{uA} A inst_1) M N inst_3
inst_7 inst_4 inst_8 inst_5
(@TensorProduct.AlgebraTensorModule.tensorTensorTensorComm.proof_1.{uM, uA, uR} R A M inst inst_1 inst_2
inst_3 inst_4 inst_5 inst_6))
(@TensorProduct.AlgebraTensorModule.tensorTensorTensorComm.proof_9.{uM, uN, uA, uR} R A M N inst inst_1 inst_2
inst_3 inst_4 inst_5 inst_6 inst_7 inst_8))
(@RingHom.id.{uA} A (@Semiring.toNonAssocSemiring.{uA} A (@CommSemiring.toSemiring.{uA} A inst_1)))
(@RingHom.id.{uA} A (@Semiring.toNonAssocSemiring.{uA} A (@CommSemiring.toSemiring.{uA} A inst_1)))
(@TensorProduct.AlgebraTensorModule.tensorTensorTensorComm.proof_7.{uA} A inst_1)
(@TensorProduct.AlgebraTensorModule.tensorTensorTensorComm.proof_7.{uA} A inst_1)
(@TensorProduct.AlgebraTensorModule.assoc.{uR, uA, uA, max uM uN, uP, uQ} R A A
(@TensorProduct.{uN, uM, uR} R inst M N inst_3 inst_7 inst_4 inst_8) P Q inst inst_1
(@CommSemiring.toSemiring.{uA} A inst_1) inst_2 inst_2
(@TensorProduct.addCommMonoid.{uN, uM, uR} R inst M N inst_3 inst_7 inst_4 inst_8)
(@TensorProduct.instModuleTensorProductToSemiringAddCommMonoid.{uN, uM, uR} R inst M N inst_3 inst_7 inst_4
inst_8)
(@TensorProduct.leftModule.{uN, uM, uA, uR} R inst A (@CommSemiring.toSemiring.{uA} A inst_1) M N inst_3
inst_7 inst_4 inst_8 inst_5
(@TensorProduct.AlgebraTensorModule.tensorTensorTensorComm.proof_1.{uM, uA, uR} R A M inst inst_1 inst_2
inst_3 inst_4 inst_5 inst_6))
(@TensorProduct.leftModule.{uN, uM, uA, uR} R inst A (@CommSemiring.toSemiring.{uA} A inst_1) M N inst_3
inst_7 inst_4 inst_8 inst_5
(@TensorProduct.AlgebraTensorModule.tensorTensorTensorComm.proof_1.{uM, uA, uR} R A M inst inst_1 inst_2
inst_3 inst_4 inst_5 inst_6))
(@TensorProduct.AlgebraTensorModule.tensorTensorTensorComm.proof_11.{uM, uN, uA, uR} R A M N inst inst_1
inst_2 inst_3 inst_4 inst_5 inst_6 inst_7 inst_8)
(@TensorProduct.AlgebraTensorModule.tensorTensorTensorComm.proof_11.{uM, uN, uA, uR} R A M N inst inst_1
inst_2 inst_3 inst_4 inst_5 inst_6 inst_7 inst_8)
(@TensorProduct.AlgebraTensorModule.tensorTensorTensorComm.proof_9.{uM, uN, uA, uR} R A M N inst inst_1 inst_2
inst_3 inst_4 inst_5 inst_6 inst_7 inst_8)
inst_9 inst_10 inst_11 inst_12 inst_13 inst_14 (@Algebra.id.{uA} A inst_1)
(@TensorProduct.AlgebraTensorModule.tensorTensorTensorComm.proof_12.{uM, uN, uA, uR} R A M N inst inst_1
inst_2 inst_3 inst_4 inst_5 inst_6 inst_7 inst_8)))
(@TensorProduct.AlgebraTensorModule.congr.{uR, uA, max (max uM uN) uP, uQ, max (max uM uN) uP, uQ} R A
(@TensorProduct.{uP, max uM uN, uA} A inst_1
(@TensorProduct.{uN, uM, uR} R inst M N inst_3 inst_7 inst_4 inst_8) P
(@TensorProduct.addCommMonoid.{uN, uM, uR} R inst M N inst_3 inst_7 inst_4 inst_8) inst_9
(@TensorProduct.leftModule.{uN, uM, uA, uR} R inst A (@CommSemiring.toSemiring.{uA} A inst_1) M N inst_3
inst_7 inst_4 inst_8 inst_5
(@TensorProduct.AlgebraTensorModule.tensorTensorTensorComm.proof_1.{uM, uA, uR} R A M inst inst_1 inst_2
inst_3 inst_4 inst_5 inst_6))
inst_11)
Q
(@TensorProduct.{uN, max uM uP, uR} R inst
(@TensorProduct.{uP, uM, uA} A inst_1 M P inst_3 inst_9 inst_5 inst_11) N
(@TensorProduct.addCommMonoid.{uP, uM, uA} A inst_1 M P inst_3 inst_9 inst_5 inst_11) inst_7
(@TensorProduct.leftModule.{uP, uM, uR, uA} A inst_1 R (@CommSemiring.toSemiring.{uR} R inst) M P inst_3
inst_9 inst_5 inst_11 inst_4
(@TensorProduct.AlgebraTensorModule.tensorTensorTensorComm.proof_3.{uM, uR, uA} R A M inst inst_1 inst_2
inst_3 inst_4 inst_5 inst_6))
inst_8)
Q inst (@CommSemiring.toSemiring.{uA} A inst_1) inst_2
(@TensorProduct.addCommMonoid.{uP, max uM uN, uA} A inst_1
(@TensorProduct.{uN, uM, uR} R inst M N inst_3 inst_7 inst_4 inst_8) P
(@TensorProduct.addCommMonoid.{uN, uM, uR} R inst M N inst_3 inst_7 inst_4 inst_8) inst_9
(@TensorProduct.leftModule.{uN, uM, uA, uR} R inst A (@CommSemiring.toSemiring.{uA} A inst_1) M N inst_3
inst_7 inst_4 inst_8 inst_5
(@TensorProduct.AlgebraTensorModule.tensorTensorTensorComm.proof_1.{uM, uA, uR} R A M inst inst_1 inst_2
inst_3 inst_4 inst_5 inst_6))
inst_11)
(@TensorProduct.leftModule.{uP, max uM uN, uR, uA} A inst_1 R (@CommSemiring.toSemiring.{uR} R inst)
(@TensorProduct.{uN, uM, uR} R inst M N inst_3 inst_7 inst_4 inst_8) P
(@TensorProduct.addCommMonoid.{uN, uM, uR} R inst M N inst_3 inst_7 inst_4 inst_8) inst_9
(@TensorProduct.leftModule.{uN, uM, uA, uR} R inst A (@CommSemiring.toSemiring.{uA} A inst_1) M N inst_3
inst_7 inst_4 inst_8 inst_5
(@TensorProduct.AlgebraTensorModule.tensorTensorTensorComm.proof_1.{uM, uA, uR} R A M inst inst_1 inst_2
inst_3 inst_4 inst_5 inst_6))
inst_11
(@TensorProduct.instModuleTensorProductToSemiringAddCommMonoid.{uN, uM, uR} R inst M N inst_3 inst_7 inst_4
inst_8)
(@TensorProduct.AlgebraTensorModule.tensorTensorTensorComm.proof_8.{uM, uN, uR, uA} R A M N inst inst_1 inst_2
inst_3 inst_4 inst_5 inst_6 inst_7 inst_8))
(@TensorProduct.leftModule.{uP, max uM uN, uA, uA} A inst_1 A (@CommSemiring.toSemiring.{uA} A inst_1)
(@TensorProduct.{uN, uM, uR} R inst M N inst_3 inst_7 inst_4 inst_8) P
(@TensorProduct.addCommMonoid.{uN, uM, uR} R inst M N inst_3 inst_7 inst_4 inst_8) inst_9
(@TensorProduct.leftModule.{uN, uM, uA, uR} R inst A (@CommSemiring.toSemiring.{uA} A inst_1) M N inst_3
inst_7 inst_4 inst_8 inst_5
(@TensorProduct.AlgebraTensorModule.tensorTensorTensorComm.proof_1.{uM, uA, uR} R A M inst inst_1 inst_2
inst_3 inst_4 inst_5 inst_6))
inst_11
(@TensorProduct.leftModule.{uN, uM, uA, uR} R inst A (@CommSemiring.toSemiring.{uA} A inst_1) M N inst_3
inst_7 inst_4 inst_8 inst_5
(@TensorProduct.AlgebraTensorModule.tensorTensorTensorComm.proof_1.{uM, uA, uR} R A M inst inst_1 inst_2
inst_3 inst_4 inst_5 inst_6))
(@TensorProduct.AlgebraTensorModule.tensorTensorTensorComm.proof_9.{uM, uN, uA, uR} R A M N inst inst_1 inst_2
inst_3 inst_4 inst_5 inst_6 inst_7 inst_8))
(@TensorProduct.AlgebraTensorModule.tensorTensorTensorComm.proof_13.{uM, uN, uP, uA, uR} R A M N P inst inst_1
inst_2 inst_3 inst_4 inst_5 inst_6 inst_7 inst_8 inst_9 inst_11)
inst_13 inst_14
(@TensorProduct.addCommMonoid.{uN, max uM uP, uR} R inst
(@TensorProduct.{uP, uM, uA} A inst_1 M P inst_3 inst_9 inst_5 inst_11) N
(@TensorProduct.addCommMonoid.{uP, uM, uA} A inst_1 M P inst_3 inst_9 inst_5 inst_11) inst_7
(@TensorProduct.leftModule.{uP, uM, uR, uA} A inst_1 R (@CommSemiring.toSemiring.{uR} R inst) M P inst_3
inst_9 inst_5 inst_11 inst_4
(@TensorProduct.AlgebraTensorModule.tensorTensorTensorComm.proof_3.{uM, uR, uA} R A M inst inst_1 inst_2
inst_3 inst_4 inst_5 inst_6))
inst_8)
(@TensorProduct.instModuleTensorProductToSemiringAddCommMonoid.{uN, max uM uP, uR} R inst
(@TensorProduct.{uP, uM, uA} A inst_1 M P inst_3 inst_9 inst_5 inst_11) N
(@TensorProduct.addCommMonoid.{uP, uM, uA} A inst_1 M P inst_3 inst_9 inst_5 inst_11) inst_7
(@TensorProduct.leftModule.{uP, uM, uR, uA} A inst_1 R (@CommSemiring.toSemiring.{uR} R inst) M P inst_3
inst_9 inst_5 inst_11 inst_4
(@TensorProduct.AlgebraTensorModule.tensorTensorTensorComm.proof_3.{uM, uR, uA} R A M inst inst_1 inst_2
inst_3 inst_4 inst_5 inst_6))
inst_8)
(@TensorProduct.leftModule.{uN, max uM uP, uA, uR} R inst A (@CommSemiring.toSemiring.{uA} A inst_1)
(@TensorProduct.{uP, uM, uA} A inst_1 M P inst_3 inst_9 inst_5 inst_11) N
(@TensorProduct.addCommMonoid.{uP, uM, uA} A inst_1 M P inst_3 inst_9 inst_5 inst_11) inst_7
(@TensorProduct.leftModule.{uP, uM, uR, uA} A inst_1 R (@CommSemiring.toSemiring.{uR} R inst) M P inst_3
inst_9 inst_5 inst_11 inst_4
(@TensorProduct.AlgebraTensorModule.tensorTensorTensorComm.proof_3.{uM, uR, uA} R A M inst inst_1 inst_2
inst_3 inst_4 inst_5 inst_6))
inst_8
(@TensorProduct.instModuleTensorProductToSemiringAddCommMonoid.{uP, uM, uA} A inst_1 M P inst_3 inst_9 inst_5
inst_11)
(@TensorProduct.AlgebraTensorModule.tensorTensorTensorComm.proof_4.{uM, uP, uA, uR} R A M P inst inst_1 inst_2
inst_3 inst_4 inst_5 inst_6 inst_9 inst_11))
(@TensorProduct.AlgebraTensorModule.tensorTensorTensorComm.proof_14.{uM, uP, uN, uA, uR} R A M N P inst inst_1
inst_2 inst_3 inst_4 inst_5 inst_6 inst_7 inst_8 inst_9 inst_11)
inst_13 inst_14
(@LinearEquiv.symm.{max (max uM uN) uP, max (max uM uN) uP, uA, uA} A A
(@TensorProduct.{uN, max uM uP, uR} R inst
(@TensorProduct.{uP, uM, uA} A inst_1 M P inst_3 inst_9 inst_5 inst_11) N
(@TensorProduct.addCommMonoid.{uP, uM, uA} A inst_1 M P inst_3 inst_9 inst_5 inst_11) inst_7
(@TensorProduct.leftModule.{uP, uM, uR, uA} A inst_1 R (@CommSemiring.toSemiring.{uR} R inst) M P inst_3
inst_9 inst_5 inst_11 inst_4
(@TensorProduct.AlgebraTensorModule.tensorTensorTensorComm.proof_3.{uM, uR, uA} R A M inst inst_1 inst_2
inst_3 inst_4 inst_5 inst_6))
inst_8)
(@TensorProduct.{uP, max uM uN, uA} A inst_1
(@TensorProduct.{uN, uM, uR} R inst M N inst_3 inst_7 inst_4 inst_8) P
(@TensorProduct.addCommMonoid.{uN, uM, uR} R inst M N inst_3 inst_7 inst_4 inst_8) inst_9
(@TensorProduct.leftModule.{uN, uM, uA, uR} R inst A (@CommSemiring.toSemiring.{uA} A inst_1) M N inst_3
inst_7 inst_4 inst_8 inst_5
(@TensorProduct.AlgebraTensorModule.tensorTensorTensorComm.proof_1.{uM, uA, uR} R A M inst inst_1 inst_2
inst_3 inst_4 inst_5 inst_6))
inst_11)
(@CommSemiring.toSemiring.{uA} A inst_1) (@CommSemiring.toSemiring.{uA} A inst_1)
(@TensorProduct.addCommMonoid.{uN, max uM uP, uR} R inst
(@TensorProduct.{uP, uM, uA} A inst_1 M P inst_3 inst_9 inst_5 inst_11) N
(@TensorProduct.addCommMonoid.{uP, uM, uA} A inst_1 M P inst_3 inst_9 inst_5 inst_11) inst_7
(@TensorProduct.leftModule.{uP, uM, uR, uA} A inst_1 R (@CommSemiring.toSemiring.{uR} R inst) M P inst_3
inst_9 inst_5 inst_11 inst_4
(@TensorProduct.AlgebraTensorModule.tensorTensorTensorComm.proof_3.{uM, uR, uA} R A M inst inst_1 inst_2
inst_3 inst_4 inst_5 inst_6))
inst_8)
(@TensorProduct.addCommMonoid.{uP, max uM uN, uA} A inst_1
(@TensorProduct.{uN, uM, uR} R inst M N inst_3 inst_7 inst_4 inst_8) P
(@TensorProduct.addCommMonoid.{uN, uM, uR} R inst M N inst_3 inst_7 inst_4 inst_8) inst_9
(@TensorProduct.leftModule.{uN, uM, uA, uR} R inst A (@CommSemiring.toSemiring.{uA} A inst_1) M N inst_3
inst_7 inst_4 inst_8 inst_5
(@TensorProduct.AlgebraTensorModule.tensorTensorTensorComm.proof_1.{uM, uA, uR} R A M inst inst_1 inst_2
inst_3 inst_4 inst_5 inst_6))
inst_11)
(@TensorProduct.leftModule.{uN, max uM uP, uA, uR} R inst A (@CommSemiring.toSemiring.{uA} A inst_1)
(@TensorProduct.{uP, uM, uA} A inst_1 M P inst_3 inst_9 inst_5 inst_11) N
(@TensorProduct.addCommMonoid.{uP, uM, uA} A inst_1 M P inst_3 inst_9 inst_5 inst_11) inst_7
(@TensorProduct.leftModule.{uP, uM, uR, uA} A inst_1 R (@CommSemiring.toSemiring.{uR} R inst) M P inst_3
inst_9 inst_5 inst_11 inst_4
(@TensorProduct.AlgebraTensorModule.tensorTensorTensorComm.proof_3.{uM, uR, uA} R A M inst inst_1 inst_2
inst_3 inst_4 inst_5 inst_6))
inst_8
(@TensorProduct.instModuleTensorProductToSemiringAddCommMonoid.{uP, uM, uA} A inst_1 M P inst_3 inst_9
inst_5 inst_11)
(@TensorProduct.AlgebraTensorModule.tensorTensorTensorComm.proof_4.{uM, uP, uA, uR} R A M P inst inst_1
inst_2 inst_3 inst_4 inst_5 inst_6 inst_9 inst_11))
(@TensorProduct.instModuleTensorProductToSemiringAddCommMonoid.{uP, max uM uN, uA} A inst_1
(@TensorProduct.{uN, uM, uR} R inst M N inst_3 inst_7 inst_4 inst_8) P
(@TensorProduct.addCommMonoid.{uN, uM, uR} R inst M N inst_3 inst_7 inst_4 inst_8) inst_9
(@TensorProduct.leftModule.{uN, uM, uA, uR} R inst A (@CommSemiring.toSemiring.{uA} A inst_1) M N inst_3
inst_7 inst_4 inst_8 inst_5
(@TensorProduct.AlgebraTensorModule.tensorTensorTensorComm.proof_1.{uM, uA, uR} R A M inst inst_1 inst_2
inst_3 inst_4 inst_5 inst_6))
inst_11)
(@RingHom.id.{uA} A (@Semiring.toNonAssocSemiring.{uA} A (@CommSemiring.toSemiring.{uA} A inst_1)))
(@RingHom.id.{uA} A (@Semiring.toNonAssocSemiring.{uA} A (@CommSemiring.toSemiring.{uA} A inst_1)))
(@TensorProduct.AlgebraTensorModule.tensorTensorTensorComm.proof_7.{uA} A inst_1)
(@TensorProduct.AlgebraTensorModule.tensorTensorTensorComm.proof_7.{uA} A inst_1)
(@TensorProduct.AlgebraTensorModule.rightComm.{uR, uA, uM, uP, uN} R A M P N inst inst_1 inst_2 inst_3 inst_4
inst_5 inst_6 inst_9 inst_11 inst_7 inst_8))
(@OfNat.ofNat.{uQ}
(@LinearEquiv.{uQ, uQ, uR, uR} R R (@CommSemiring.toSemiring.{uR} R inst)
(@CommSemiring.toSemiring.{uR} R inst)
(@RingHom.id.{uR} R (@Semiring.toNonAssocSemiring.{uR} R (@CommSemiring.toSemiring.{uR} R inst)))
(@RingHom.id.{uR} R (@Semiring.toNonAssocSemiring.{uR} R (@CommSemiring.toSemiring.{uR} R inst)))
(@TensorProduct.AlgebraTensorModule.tensorTensorTensorComm.proof_15.{uR} R inst)
(@TensorProduct.AlgebraTensorModule.tensorTensorTensorComm.proof_15.{uR} R inst) Q Q inst_13 inst_13 inst_14
inst_14)
1
(@One.toOfNat1.{uQ}
(@LinearEquiv.{uQ, uQ, uR, uR} R R (@CommSemiring.toSemiring.{uR} R inst)
(@CommSemiring.toSemiring.{uR} R inst)
(@RingHom.id.{uR} R (@Semiring.toNonAssocSemiring.{uR} R (@CommSemiring.toSemiring.{uR} R inst)))
(@RingHom.id.{uR} R (@Semiring.toNonAssocSemiring.{uR} R (@CommSemiring.toSemiring.{uR} R inst)))
(@TensorProduct.AlgebraTensorModule.tensorTensorTensorComm.proof_15.{uR} R inst)
(@TensorProduct.AlgebraTensorModule.tensorTensorTensorComm.proof_15.{uR} R inst) Q Q inst_13 inst_13
inst_14 inst_14)
(@InvOneClass.toOne.{uQ}
(@LinearEquiv.{uQ, uQ, uR, uR} R R (@CommSemiring.toSemiring.{uR} R inst)
(@CommSemiring.toSemiring.{uR} R inst)
(@RingHom.id.{uR} R (@Semiring.toNonAssocSemiring.{uR} R (@CommSemiring.toSemiring.{uR} R inst)))
(@RingHom.id.{uR} R (@Semiring.toNonAssocSemiring.{uR} R (@CommSemiring.toSemiring.{uR} R inst)))
(@TensorProduct.AlgebraTensorModule.tensorTensorTensorComm.proof_15.{uR} R inst)
(@TensorProduct.AlgebraTensorModule.tensorTensorTensorComm.proof_15.{uR} R inst) Q Q inst_13 inst_13
inst_14 inst_14)
(@DivInvOneMonoid.toInvOneClass.{uQ}
(@LinearEquiv.{uQ, uQ, uR, uR} R R (@CommSemiring.toSemiring.{uR} R inst)
(@CommSemiring.toSemiring.{uR} R inst)
(@RingHom.id.{uR} R (@Semiring.toNonAssocSemiring.{uR} R (@CommSemiring.toSemiring.{uR} R inst)))
(@RingHom.id.{uR} R (@Semiring.toNonAssocSemiring.{uR} R (@CommSemiring.toSemiring.{uR} R inst)))
(@TensorProduct.AlgebraTensorModule.tensorTensorTensorComm.proof_15.{uR} R inst)
(@TensorProduct.AlgebraTensorModule.tensorTensorTensorComm.proof_15.{uR} R inst) Q Q inst_13 inst_13
inst_14 inst_14)
(@DivisionMonoid.toDivInvOneMonoid.{uQ}
(@LinearEquiv.{uQ, uQ, uR, uR} R R (@CommSemiring.toSemiring.{uR} R inst)
(@CommSemiring.toSemiring.{uR} R inst)
(@RingHom.id.{uR} R (@Semiring.toNonAssocSemiring.{uR} R (@CommSemiring.toSemiring.{uR} R inst)))
(@RingHom.id.{uR} R (@Semiring.toNonAssocSemiring.{uR} R (@CommSemiring.toSemiring.{uR} R inst)))
(@TensorProduct.AlgebraTensorModule.tensorTensorTensorComm.proof_15.{uR} R inst)
(@TensorProduct.AlgebraTensorModule.tensorTensorTensorComm.proof_15.{uR} R inst) Q Q inst_13 inst_13
inst_14 inst_14)
(@Group.toDivisionMonoid.{uQ}
(@LinearEquiv.{uQ, uQ, uR, uR} R R (@CommSemiring.toSemiring.{uR} R inst)
(@CommSemiring.toSemiring.{uR} R inst)
(@RingHom.id.{uR} R (@Semiring.toNonAssocSemiring.{uR} R (@CommSemiring.toSemiring.{uR} R inst)))
(@RingHom.id.{uR} R (@Semiring.toNonAssocSemiring.{uR} R (@CommSemiring.toSemiring.{uR} R inst)))
(@TensorProduct.AlgebraTensorModule.tensorTensorTensorComm.proof_15.{uR} R inst)
(@TensorProduct.AlgebraTensorModule.tensorTensorTensorComm.proof_15.{uR} R inst) Q Q inst_13
inst_13 inst_14 inst_14)
(@LinearEquiv.automorphismGroup.{uQ, uR} R Q (@CommSemiring.toSemiring.{uR} R inst) inst_13
inst_14)))))))))
(@TensorProduct.AlgebraTensorModule.assoc.{uR, uR, uA, max uM uP, uN, uQ} R R A
(@TensorProduct.{uP, uM, uA} A inst_1 M P inst_3 inst_9 inst_5 inst_11) N Q inst inst
(@CommSemiring.toSemiring.{uA} A inst_1) (@Algebra.id.{uR} R inst) inst_2
(@TensorProduct.addCommMonoid.{uP, uM, uA} A inst_1 M P inst_3 inst_9 inst_5 inst_11)
(@TensorProduct.leftModule.{uP, uM, uR, uA} A inst_1 R (@CommSemiring.toSemiring.{uR} R inst) M P inst_3 inst_9
inst_5 inst_11 inst_4
(@TensorProduct.AlgebraTensorModule.tensorTensorTensorComm.proof_3.{uM, uR, uA} R A M inst inst_1 inst_2 inst_3
inst_4 inst_5 inst_6))
(@TensorProduct.leftModule.{uP, uM, uR, uA} A inst_1 R (@CommSemiring.toSemiring.{uR} R inst) M P inst_3 inst_9
inst_5 inst_11 inst_4
(@TensorProduct.AlgebraTensorModule.tensorTensorTensorComm.proof_3.{uM, uR, uA} R A M inst inst_1 inst_2 inst_3
inst_4 inst_5 inst_6))
(@TensorProduct.instModuleTensorProductToSemiringAddCommMonoid.{uP, uM, uA} A inst_1 M P inst_3 inst_9 inst_5
inst_11)
(@TensorProduct.AlgebraTensorModule.tensorTensorTensorComm.proof_16.{uM, uP, uR, uA} R A M P inst inst_1 inst_2
inst_3 inst_4 inst_5 inst_6 inst_9 inst_10 inst_11 inst_12)
(@TensorProduct.AlgebraTensorModule.tensorTensorTensorComm.proof_17.{uM, uP, uA, uR} R A M P inst inst_1 inst_2
inst_3 inst_4 inst_5 inst_6 inst_9 inst_11)
(@TensorProduct.AlgebraTensorModule.tensorTensorTensorComm.proof_4.{uM, uP, uA, uR} R A M P inst inst_1 inst_2
inst_3 inst_4 inst_5 inst_6 inst_9 inst_11)
inst_7 inst_8 inst_8
(@TensorProduct.AlgebraTensorModule.tensorTensorTensorComm.proof_18.{uN, uR} R N inst inst_7 inst_8) inst_13
inst_14 inst_2
(@TensorProduct.AlgebraTensorModule.tensorTensorTensorComm.proof_17.{uM, uP, uA, uR} R A M P inst inst_1 inst_2
inst_3 inst_4 inst_5 inst_6 inst_9 inst_11))
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment