Created
July 25, 2023 20:28
-
-
Save mattrobball/4547c55d6a23e079e8c5ca5598ded641 to your computer and use it in GitHub Desktop.
Semi-ring instances
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| def Algebra.TensorProduct.instSemiring.{u, v₁, v₂} : {R : Type u} → | |
| [inst : CommSemiring.{u} R] → | |
| {A : Type v₁} → | |
| [inst_1 : Semiring.{v₁} A] → | |
| [inst_2 : @Algebra.{u, v₁} R A inst inst_1] → | |
| {B : Type v₂} → | |
| [inst_3 : Semiring.{v₂} B] → | |
| [inst_4 : @Algebra.{u, v₂} R B inst inst_3] → | |
| Semiring.{max v₂ v₁} | |
| (@TensorProduct.{u, v₁, v₂} R inst A B | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₁} A | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₁} A | |
| (@Semiring.toNonAssocSemiring.{v₁} A inst_1))) | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₂} B | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₂} B | |
| (@Semiring.toNonAssocSemiring.{v₂} B inst_3))) | |
| (@Algebra.toModule.{u, v₁} R A inst inst_1 inst_2) | |
| (@Algebra.toModule.{u, v₂} R B inst inst_3 inst_4)) := | |
| fun {R : Type u} [inst : CommSemiring.{u} R] {A : Type v₁} [inst_1 : Semiring.{v₁} A] | |
| [inst_2 : @Algebra.{u, v₁} R A inst inst_1] {B : Type v₂} [inst_3 : Semiring.{v₂} B] | |
| [inst_4 : @Algebra.{u, v₂} R B inst inst_3] ↦ | |
| @Semiring.mk.{max v₁ v₂} | |
| (@TensorProduct.{u, v₁, v₂} R inst A B | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₁} A | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₁} A (@Semiring.toNonAssocSemiring.{v₁} A inst_1))) | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₂} B | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₂} B (@Semiring.toNonAssocSemiring.{v₂} B inst_3))) | |
| (@Algebra.toModule.{u, v₁} R A inst inst_1 inst_2) (@Algebra.toModule.{u, v₂} R B inst inst_3 inst_4)) | |
| (@NonUnitalSemiring.mk.{max v₁ v₂} | |
| (@TensorProduct.{u, v₁, v₂} R inst A B | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₁} A | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₁} A (@Semiring.toNonAssocSemiring.{v₁} A inst_1))) | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₂} B | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₂} B (@Semiring.toNonAssocSemiring.{v₂} B inst_3))) | |
| (@Algebra.toModule.{u, v₁} R A inst inst_1 inst_2) (@Algebra.toModule.{u, v₂} R B inst inst_3 inst_4)) | |
| (@NonUnitalNonAssocSemiring.mk.{max v₁ v₂} | |
| (@TensorProduct.{u, v₁, v₂} R inst A B | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₁} A | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₁} A (@Semiring.toNonAssocSemiring.{v₁} A inst_1))) | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₂} B | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₂} B (@Semiring.toNonAssocSemiring.{v₂} B inst_3))) | |
| (@Algebra.toModule.{u, v₁} R A inst inst_1 inst_2) (@Algebra.toModule.{u, v₂} R B inst inst_3 inst_4)) | |
| (@inferInstance.{max (v₁ + 1) (v₂ + 1)} | |
| (AddCommMonoid.{max v₁ v₂} | |
| (@TensorProduct.{u, v₁, v₂} R inst A B | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₁} A | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₁} A (@Semiring.toNonAssocSemiring.{v₁} A inst_1))) | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₂} B | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₂} B (@Semiring.toNonAssocSemiring.{v₂} B inst_3))) | |
| (@Algebra.toModule.{u, v₁} R A inst inst_1 inst_2) (@Algebra.toModule.{u, v₂} R B inst inst_3 inst_4))) | |
| (@Algebra.TensorProduct.instAddCommMonoidTensorProductToAddCommMonoidToNonUnitalNonAssocSemiringToNonAssocSemiringToAddCommMonoidToNonUnitalNonAssocSemiringToNonAssocSemiringToModuleToModule.{u, | |
| v₁, v₂} | |
| R inst A inst_1 inst_2 B inst_3 inst_4)) | |
| (@Mul.mk.{max v₁ v₂} | |
| (@TensorProduct.{u, v₁, v₂} R inst A B | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₁} A | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₁} A (@Semiring.toNonAssocSemiring.{v₁} A inst_1))) | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₂} B | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₂} B (@Semiring.toNonAssocSemiring.{v₂} B inst_3))) | |
| (@Algebra.toModule.{u, v₁} R A inst inst_1 inst_2) (@Algebra.toModule.{u, v₂} R B inst inst_3 inst_4)) | |
| fun | |
| (a b : | |
| @TensorProduct.{u, v₁, v₂} R inst A B | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₁} A | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₁} A (@Semiring.toNonAssocSemiring.{v₁} A inst_1))) | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₂} B | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₂} B (@Semiring.toNonAssocSemiring.{v₂} B inst_3))) | |
| (@Algebra.toModule.{u, v₁} R A inst inst_1 inst_2) (@Algebra.toModule.{u, v₂} R B inst inst_3 inst_4)) ↦ | |
| @FunLike.coe.{max (v₁ + 1) (v₂ + 1), max (v₁ + 1) (v₂ + 1), max (v₁ + 1) (v₂ + 1)} | |
| ((fun | |
| (x : | |
| @TensorProduct.{u, v₁, v₂} R inst A B | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₁} A | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₁} A | |
| (@Semiring.toNonAssocSemiring.{v₁} A inst_1))) | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₂} B | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₂} B | |
| (@Semiring.toNonAssocSemiring.{v₂} B inst_3))) | |
| (@Algebra.toModule.{u, v₁} R A inst inst_1 inst_2) | |
| (@Algebra.toModule.{u, v₂} R B inst inst_3 inst_4)) ↦ | |
| @LinearMap.{u, u, max v₂ v₁, max v₂ v₁} R R (@CommSemiring.toSemiring.{u} R inst) | |
| (@CommSemiring.toSemiring.{u} R inst) | |
| (@RingHom.id.{u} R (@Semiring.toNonAssocSemiring.{u} R (@CommSemiring.toSemiring.{u} R inst))) | |
| (@TensorProduct.{u, v₁, v₂} R inst A B | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₁} A | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₁} A | |
| (@Semiring.toNonAssocSemiring.{v₁} A inst_1))) | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₂} B | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₂} B | |
| (@Semiring.toNonAssocSemiring.{v₂} B inst_3))) | |
| (@Algebra.toModule.{u, v₁} R A inst inst_1 inst_2) | |
| (@Algebra.toModule.{u, v₂} R B inst inst_3 inst_4)) | |
| (@TensorProduct.{u, v₁, v₂} R inst A B | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₁} A | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₁} A | |
| (@Semiring.toNonAssocSemiring.{v₁} A inst_1))) | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₂} B | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₂} B | |
| (@Semiring.toNonAssocSemiring.{v₂} B inst_3))) | |
| (@Algebra.toModule.{u, v₁} R A inst inst_1 inst_2) | |
| (@Algebra.toModule.{u, v₂} R B inst inst_3 inst_4)) | |
| (@TensorProduct.addCommMonoid.{u, v₁, v₂} R inst A B | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₁} A | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₁} A | |
| (@Semiring.toNonAssocSemiring.{v₁} A inst_1))) | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₂} B | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₂} B | |
| (@Semiring.toNonAssocSemiring.{v₂} B inst_3))) | |
| (@Algebra.toModule.{u, v₁} R A inst inst_1 inst_2) | |
| (@Algebra.toModule.{u, v₂} R B inst inst_3 inst_4)) | |
| (@TensorProduct.addCommMonoid.{u, v₁, v₂} R inst A B | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₁} A | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₁} A | |
| (@Semiring.toNonAssocSemiring.{v₁} A inst_1))) | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₂} B | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₂} B | |
| (@Semiring.toNonAssocSemiring.{v₂} B inst_3))) | |
| (@Algebra.toModule.{u, v₁} R A inst inst_1 inst_2) | |
| (@Algebra.toModule.{u, v₂} R B inst inst_3 inst_4)) | |
| (@TensorProduct.instModuleTensorProductToSemiringAddCommMonoid.{u, v₁, v₂} R inst A B | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₁} A | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₁} A | |
| (@Semiring.toNonAssocSemiring.{v₁} A inst_1))) | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₂} B | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₂} B | |
| (@Semiring.toNonAssocSemiring.{v₂} B inst_3))) | |
| (@Algebra.toModule.{u, v₁} R A inst inst_1 inst_2) | |
| (@Algebra.toModule.{u, v₂} R B inst inst_3 inst_4)) | |
| (@TensorProduct.instModuleTensorProductToSemiringAddCommMonoid.{u, v₁, v₂} R inst A B | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₁} A | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₁} A | |
| (@Semiring.toNonAssocSemiring.{v₁} A inst_1))) | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₂} B | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₂} B | |
| (@Semiring.toNonAssocSemiring.{v₂} B inst_3))) | |
| (@Algebra.toModule.{u, v₁} R A inst inst_1 inst_2) | |
| (@Algebra.toModule.{u, v₂} R B inst inst_3 inst_4))) | |
| a) | |
| (@TensorProduct.{u, v₁, v₂} R inst A B | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₁} A | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₁} A (@Semiring.toNonAssocSemiring.{v₁} A inst_1))) | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₂} B | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₂} B (@Semiring.toNonAssocSemiring.{v₂} B inst_3))) | |
| (@Algebra.toModule.{u, v₁} R A inst inst_1 inst_2) (@Algebra.toModule.{u, v₂} R B inst inst_3 inst_4)) | |
| (fun | |
| (a : | |
| @TensorProduct.{u, v₁, v₂} R inst A B | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₁} A | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₁} A | |
| (@Semiring.toNonAssocSemiring.{v₁} A inst_1))) | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₂} B | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₂} B | |
| (@Semiring.toNonAssocSemiring.{v₂} B inst_3))) | |
| (@Algebra.toModule.{u, v₁} R A inst inst_1 inst_2) | |
| (@Algebra.toModule.{u, v₂} R B inst inst_3 inst_4)) ↦ | |
| (fun | |
| (x : | |
| @TensorProduct.{u, v₁, v₂} R inst A B | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₁} A | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₁} A | |
| (@Semiring.toNonAssocSemiring.{v₁} A inst_1))) | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₂} B | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₂} B | |
| (@Semiring.toNonAssocSemiring.{v₂} B inst_3))) | |
| (@Algebra.toModule.{u, v₁} R A inst inst_1 inst_2) | |
| (@Algebra.toModule.{u, v₂} R B inst inst_3 inst_4)) ↦ | |
| @TensorProduct.{u, v₁, v₂} R inst A B | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₁} A | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₁} A | |
| (@Semiring.toNonAssocSemiring.{v₁} A inst_1))) | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₂} B | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₂} B | |
| (@Semiring.toNonAssocSemiring.{v₂} B inst_3))) | |
| (@Algebra.toModule.{u, v₁} R A inst inst_1 inst_2) | |
| (@Algebra.toModule.{u, v₂} R B inst inst_3 inst_4)) | |
| a) | |
| (@LinearMap.instFunLikeLinearMap.{u, u, max v₁ v₂, max v₁ v₂} R R | |
| (@TensorProduct.{u, v₁, v₂} R inst A B | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₁} A | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₁} A (@Semiring.toNonAssocSemiring.{v₁} A inst_1))) | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₂} B | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₂} B (@Semiring.toNonAssocSemiring.{v₂} B inst_3))) | |
| (@Algebra.toModule.{u, v₁} R A inst inst_1 inst_2) (@Algebra.toModule.{u, v₂} R B inst inst_3 inst_4)) | |
| (@TensorProduct.{u, v₁, v₂} R inst A B | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₁} A | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₁} A (@Semiring.toNonAssocSemiring.{v₁} A inst_1))) | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₂} B | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₂} B (@Semiring.toNonAssocSemiring.{v₂} B inst_3))) | |
| (@Algebra.toModule.{u, v₁} R A inst inst_1 inst_2) (@Algebra.toModule.{u, v₂} R B inst inst_3 inst_4)) | |
| (@CommSemiring.toSemiring.{u} R inst) (@CommSemiring.toSemiring.{u} R inst) | |
| (@TensorProduct.addCommMonoid.{u, v₁, v₂} R inst A B | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₁} A | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₁} A (@Semiring.toNonAssocSemiring.{v₁} A inst_1))) | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₂} B | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₂} B (@Semiring.toNonAssocSemiring.{v₂} B inst_3))) | |
| (@Algebra.toModule.{u, v₁} R A inst inst_1 inst_2) (@Algebra.toModule.{u, v₂} R B inst inst_3 inst_4)) | |
| (@TensorProduct.addCommMonoid.{u, v₁, v₂} R inst A B | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₁} A | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₁} A (@Semiring.toNonAssocSemiring.{v₁} A inst_1))) | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₂} B | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₂} B (@Semiring.toNonAssocSemiring.{v₂} B inst_3))) | |
| (@Algebra.toModule.{u, v₁} R A inst inst_1 inst_2) (@Algebra.toModule.{u, v₂} R B inst inst_3 inst_4)) | |
| (@TensorProduct.instModuleTensorProductToSemiringAddCommMonoid.{u, v₁, v₂} R inst A B | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₁} A | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₁} A (@Semiring.toNonAssocSemiring.{v₁} A inst_1))) | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₂} B | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₂} B (@Semiring.toNonAssocSemiring.{v₂} B inst_3))) | |
| (@Algebra.toModule.{u, v₁} R A inst inst_1 inst_2) (@Algebra.toModule.{u, v₂} R B inst inst_3 inst_4)) | |
| (@TensorProduct.instModuleTensorProductToSemiringAddCommMonoid.{u, v₁, v₂} R inst A B | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₁} A | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₁} A (@Semiring.toNonAssocSemiring.{v₁} A inst_1))) | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₂} B | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₂} B (@Semiring.toNonAssocSemiring.{v₂} B inst_3))) | |
| (@Algebra.toModule.{u, v₁} R A inst inst_1 inst_2) (@Algebra.toModule.{u, v₂} R B inst inst_3 inst_4)) | |
| (@RingHom.id.{u} R (@Semiring.toNonAssocSemiring.{u} R (@CommSemiring.toSemiring.{u} R inst)))) | |
| (@FunLike.coe.{max (v₂ + 1) (v₁ + 1), max (v₂ + 1) (v₁ + 1), max (v₂ + 1) (v₁ + 1)} | |
| (@LinearMap.{u, u, max v₂ v₁, max v₂ v₁} R R (@CommSemiring.toSemiring.{u} R inst) | |
| (@CommSemiring.toSemiring.{u} R inst) | |
| (@RingHom.id.{u} R (@Semiring.toNonAssocSemiring.{u} R (@CommSemiring.toSemiring.{u} R inst))) | |
| (@TensorProduct.{u, v₁, v₂} R inst A B | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₁} A | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₁} A (@Semiring.toNonAssocSemiring.{v₁} A inst_1))) | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₂} B | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₂} B (@Semiring.toNonAssocSemiring.{v₂} B inst_3))) | |
| (@Algebra.toModule.{u, v₁} R A inst inst_1 inst_2) (@Algebra.toModule.{u, v₂} R B inst inst_3 inst_4)) | |
| (@LinearMap.{u, u, max v₂ v₁, max v₂ v₁} R R (@CommSemiring.toSemiring.{u} R inst) | |
| (@CommSemiring.toSemiring.{u} R inst) | |
| (@RingHom.id.{u} R (@Semiring.toNonAssocSemiring.{u} R (@CommSemiring.toSemiring.{u} R inst))) | |
| (@TensorProduct.{u, v₁, v₂} R inst A B | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₁} A | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₁} A | |
| (@Semiring.toNonAssocSemiring.{v₁} A inst_1))) | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₂} B | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₂} B | |
| (@Semiring.toNonAssocSemiring.{v₂} B inst_3))) | |
| (@Algebra.toModule.{u, v₁} R A inst inst_1 inst_2) | |
| (@Algebra.toModule.{u, v₂} R B inst inst_3 inst_4)) | |
| (@TensorProduct.{u, v₁, v₂} R inst A B | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₁} A | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₁} A | |
| (@Semiring.toNonAssocSemiring.{v₁} A inst_1))) | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₂} B | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₂} B | |
| (@Semiring.toNonAssocSemiring.{v₂} B inst_3))) | |
| (@Algebra.toModule.{u, v₁} R A inst inst_1 inst_2) | |
| (@Algebra.toModule.{u, v₂} R B inst inst_3 inst_4)) | |
| (@TensorProduct.addCommMonoid.{u, v₁, v₂} R inst A B | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₁} A | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₁} A | |
| (@Semiring.toNonAssocSemiring.{v₁} A inst_1))) | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₂} B | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₂} B | |
| (@Semiring.toNonAssocSemiring.{v₂} B inst_3))) | |
| (@Algebra.toModule.{u, v₁} R A inst inst_1 inst_2) | |
| (@Algebra.toModule.{u, v₂} R B inst inst_3 inst_4)) | |
| (@TensorProduct.addCommMonoid.{u, v₁, v₂} R inst A B | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₁} A | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₁} A | |
| (@Semiring.toNonAssocSemiring.{v₁} A inst_1))) | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₂} B | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₂} B | |
| (@Semiring.toNonAssocSemiring.{v₂} B inst_3))) | |
| (@Algebra.toModule.{u, v₁} R A inst inst_1 inst_2) | |
| (@Algebra.toModule.{u, v₂} R B inst inst_3 inst_4)) | |
| (@TensorProduct.instModuleTensorProductToSemiringAddCommMonoid.{u, v₁, v₂} R inst A B | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₁} A | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₁} A | |
| (@Semiring.toNonAssocSemiring.{v₁} A inst_1))) | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₂} B | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₂} B | |
| (@Semiring.toNonAssocSemiring.{v₂} B inst_3))) | |
| (@Algebra.toModule.{u, v₁} R A inst inst_1 inst_2) | |
| (@Algebra.toModule.{u, v₂} R B inst inst_3 inst_4)) | |
| (@TensorProduct.instModuleTensorProductToSemiringAddCommMonoid.{u, v₁, v₂} R inst A B | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₁} A | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₁} A | |
| (@Semiring.toNonAssocSemiring.{v₁} A inst_1))) | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₂} B | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₂} B | |
| (@Semiring.toNonAssocSemiring.{v₂} B inst_3))) | |
| (@Algebra.toModule.{u, v₁} R A inst inst_1 inst_2) | |
| (@Algebra.toModule.{u, v₂} R B inst inst_3 inst_4))) | |
| (@TensorProduct.addCommMonoid.{u, v₁, v₂} R inst A B | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₁} A | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₁} A (@Semiring.toNonAssocSemiring.{v₁} A inst_1))) | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₂} B | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₂} B (@Semiring.toNonAssocSemiring.{v₂} B inst_3))) | |
| (@Algebra.toModule.{u, v₁} R A inst inst_1 inst_2) (@Algebra.toModule.{u, v₂} R B inst inst_3 inst_4)) | |
| (@LinearMap.addCommMonoid.{u, u, max v₁ v₂, max v₁ v₂} R R | |
| (@TensorProduct.{u, v₁, v₂} R inst A B | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₁} A | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₁} A | |
| (@Semiring.toNonAssocSemiring.{v₁} A inst_1))) | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₂} B | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₂} B | |
| (@Semiring.toNonAssocSemiring.{v₂} B inst_3))) | |
| (@Algebra.toModule.{u, v₁} R A inst inst_1 inst_2) | |
| (@Algebra.toModule.{u, v₂} R B inst inst_3 inst_4)) | |
| (@TensorProduct.{u, v₁, v₂} R inst A B | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₁} A | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₁} A | |
| (@Semiring.toNonAssocSemiring.{v₁} A inst_1))) | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₂} B | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₂} B | |
| (@Semiring.toNonAssocSemiring.{v₂} B inst_3))) | |
| (@Algebra.toModule.{u, v₁} R A inst inst_1 inst_2) | |
| (@Algebra.toModule.{u, v₂} R B inst inst_3 inst_4)) | |
| (@CommSemiring.toSemiring.{u} R inst) (@CommSemiring.toSemiring.{u} R inst) | |
| (@TensorProduct.addCommMonoid.{u, v₁, v₂} R inst A B | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₁} A | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₁} A | |
| (@Semiring.toNonAssocSemiring.{v₁} A inst_1))) | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₂} B | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₂} B | |
| (@Semiring.toNonAssocSemiring.{v₂} B inst_3))) | |
| (@Algebra.toModule.{u, v₁} R A inst inst_1 inst_2) | |
| (@Algebra.toModule.{u, v₂} R B inst inst_3 inst_4)) | |
| (@TensorProduct.addCommMonoid.{u, v₁, v₂} R inst A B | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₁} A | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₁} A | |
| (@Semiring.toNonAssocSemiring.{v₁} A inst_1))) | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₂} B | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₂} B | |
| (@Semiring.toNonAssocSemiring.{v₂} B inst_3))) | |
| (@Algebra.toModule.{u, v₁} R A inst inst_1 inst_2) | |
| (@Algebra.toModule.{u, v₂} R B inst inst_3 inst_4)) | |
| (@TensorProduct.instModuleTensorProductToSemiringAddCommMonoid.{u, v₁, v₂} R inst A B | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₁} A | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₁} A | |
| (@Semiring.toNonAssocSemiring.{v₁} A inst_1))) | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₂} B | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₂} B | |
| (@Semiring.toNonAssocSemiring.{v₂} B inst_3))) | |
| (@Algebra.toModule.{u, v₁} R A inst inst_1 inst_2) | |
| (@Algebra.toModule.{u, v₂} R B inst inst_3 inst_4)) | |
| (@TensorProduct.instModuleTensorProductToSemiringAddCommMonoid.{u, v₁, v₂} R inst A B | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₁} A | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₁} A | |
| (@Semiring.toNonAssocSemiring.{v₁} A inst_1))) | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₂} B | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₂} B | |
| (@Semiring.toNonAssocSemiring.{v₂} B inst_3))) | |
| (@Algebra.toModule.{u, v₁} R A inst inst_1 inst_2) | |
| (@Algebra.toModule.{u, v₂} R B inst inst_3 inst_4)) | |
| (@RingHom.id.{u} R (@Semiring.toNonAssocSemiring.{u} R (@CommSemiring.toSemiring.{u} R inst)))) | |
| (@TensorProduct.instModuleTensorProductToSemiringAddCommMonoid.{u, v₁, v₂} R inst A B | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₁} A | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₁} A (@Semiring.toNonAssocSemiring.{v₁} A inst_1))) | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₂} B | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₂} B (@Semiring.toNonAssocSemiring.{v₂} B inst_3))) | |
| (@Algebra.toModule.{u, v₁} R A inst inst_1 inst_2) (@Algebra.toModule.{u, v₂} R B inst inst_3 inst_4)) | |
| (@LinearMap.module.{u, u, u, max v₁ v₂, max v₁ v₂} R R R | |
| (@TensorProduct.{u, v₁, v₂} R inst A B | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₁} A | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₁} A | |
| (@Semiring.toNonAssocSemiring.{v₁} A inst_1))) | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₂} B | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₂} B | |
| (@Semiring.toNonAssocSemiring.{v₂} B inst_3))) | |
| (@Algebra.toModule.{u, v₁} R A inst inst_1 inst_2) | |
| (@Algebra.toModule.{u, v₂} R B inst inst_3 inst_4)) | |
| (@TensorProduct.{u, v₁, v₂} R inst A B | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₁} A | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₁} A | |
| (@Semiring.toNonAssocSemiring.{v₁} A inst_1))) | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₂} B | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₂} B | |
| (@Semiring.toNonAssocSemiring.{v₂} B inst_3))) | |
| (@Algebra.toModule.{u, v₁} R A inst inst_1 inst_2) | |
| (@Algebra.toModule.{u, v₂} R B inst inst_3 inst_4)) | |
| (@CommSemiring.toSemiring.{u} R inst) (@CommSemiring.toSemiring.{u} R inst) | |
| (@TensorProduct.addCommMonoid.{u, v₁, v₂} R inst A B | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₁} A | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₁} A | |
| (@Semiring.toNonAssocSemiring.{v₁} A inst_1))) | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₂} B | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₂} B | |
| (@Semiring.toNonAssocSemiring.{v₂} B inst_3))) | |
| (@Algebra.toModule.{u, v₁} R A inst inst_1 inst_2) | |
| (@Algebra.toModule.{u, v₂} R B inst inst_3 inst_4)) | |
| (@TensorProduct.addCommMonoid.{u, v₁, v₂} R inst A B | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₁} A | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₁} A | |
| (@Semiring.toNonAssocSemiring.{v₁} A inst_1))) | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₂} B | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₂} B | |
| (@Semiring.toNonAssocSemiring.{v₂} B inst_3))) | |
| (@Algebra.toModule.{u, v₁} R A inst inst_1 inst_2) | |
| (@Algebra.toModule.{u, v₂} R B inst inst_3 inst_4)) | |
| (@TensorProduct.instModuleTensorProductToSemiringAddCommMonoid.{u, v₁, v₂} R inst A B | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₁} A | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₁} A | |
| (@Semiring.toNonAssocSemiring.{v₁} A inst_1))) | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₂} B | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₂} B | |
| (@Semiring.toNonAssocSemiring.{v₂} B inst_3))) | |
| (@Algebra.toModule.{u, v₁} R A inst inst_1 inst_2) | |
| (@Algebra.toModule.{u, v₂} R B inst inst_3 inst_4)) | |
| (@TensorProduct.instModuleTensorProductToSemiringAddCommMonoid.{u, v₁, v₂} R inst A B | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₁} A | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₁} A | |
| (@Semiring.toNonAssocSemiring.{v₁} A inst_1))) | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₂} B | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₂} B | |
| (@Semiring.toNonAssocSemiring.{v₂} B inst_3))) | |
| (@Algebra.toModule.{u, v₁} R A inst inst_1 inst_2) | |
| (@Algebra.toModule.{u, v₂} R B inst inst_3 inst_4)) | |
| (@RingHom.id.{u} R (@Semiring.toNonAssocSemiring.{u} R (@CommSemiring.toSemiring.{u} R inst))) | |
| (@CommSemiring.toSemiring.{u} R inst) | |
| (@TensorProduct.instModuleTensorProductToSemiringAddCommMonoid.{u, v₁, v₂} R inst A B | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₁} A | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₁} A | |
| (@Semiring.toNonAssocSemiring.{v₁} A inst_1))) | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₂} B | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₂} B | |
| (@Semiring.toNonAssocSemiring.{v₂} B inst_3))) | |
| (@Algebra.toModule.{u, v₁} R A inst inst_1 inst_2) | |
| (@Algebra.toModule.{u, v₂} R B inst inst_3 inst_4)) | |
| (@Algebra.TensorProduct.instSemiring.proof_1.{u, v₁, v₂} R inst A inst_1 inst_2 B inst_3 inst_4))) | |
| (@TensorProduct.{u, v₁, v₂} R inst A B | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₁} A | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₁} A (@Semiring.toNonAssocSemiring.{v₁} A inst_1))) | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₂} B | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₂} B (@Semiring.toNonAssocSemiring.{v₂} B inst_3))) | |
| (@Algebra.toModule.{u, v₁} R A inst inst_1 inst_2) (@Algebra.toModule.{u, v₂} R B inst inst_3 inst_4)) | |
| (fun | |
| (a : | |
| @TensorProduct.{u, v₁, v₂} R inst A B | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₁} A | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₁} A | |
| (@Semiring.toNonAssocSemiring.{v₁} A inst_1))) | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₂} B | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₂} B | |
| (@Semiring.toNonAssocSemiring.{v₂} B inst_3))) | |
| (@Algebra.toModule.{u, v₁} R A inst inst_1 inst_2) | |
| (@Algebra.toModule.{u, v₂} R B inst inst_3 inst_4)) ↦ | |
| (fun | |
| (x : | |
| @TensorProduct.{u, v₁, v₂} R inst A B | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₁} A | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₁} A | |
| (@Semiring.toNonAssocSemiring.{v₁} A inst_1))) | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₂} B | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₂} B | |
| (@Semiring.toNonAssocSemiring.{v₂} B inst_3))) | |
| (@Algebra.toModule.{u, v₁} R A inst inst_1 inst_2) | |
| (@Algebra.toModule.{u, v₂} R B inst inst_3 inst_4)) ↦ | |
| @LinearMap.{u, u, max v₂ v₁, max v₂ v₁} R R (@CommSemiring.toSemiring.{u} R inst) | |
| (@CommSemiring.toSemiring.{u} R inst) | |
| (@RingHom.id.{u} R (@Semiring.toNonAssocSemiring.{u} R (@CommSemiring.toSemiring.{u} R inst))) | |
| (@TensorProduct.{u, v₁, v₂} R inst A B | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₁} A | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₁} A | |
| (@Semiring.toNonAssocSemiring.{v₁} A inst_1))) | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₂} B | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₂} B | |
| (@Semiring.toNonAssocSemiring.{v₂} B inst_3))) | |
| (@Algebra.toModule.{u, v₁} R A inst inst_1 inst_2) | |
| (@Algebra.toModule.{u, v₂} R B inst inst_3 inst_4)) | |
| (@TensorProduct.{u, v₁, v₂} R inst A B | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₁} A | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₁} A | |
| (@Semiring.toNonAssocSemiring.{v₁} A inst_1))) | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₂} B | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₂} B | |
| (@Semiring.toNonAssocSemiring.{v₂} B inst_3))) | |
| (@Algebra.toModule.{u, v₁} R A inst inst_1 inst_2) | |
| (@Algebra.toModule.{u, v₂} R B inst inst_3 inst_4)) | |
| (@TensorProduct.addCommMonoid.{u, v₁, v₂} R inst A B | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₁} A | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₁} A | |
| (@Semiring.toNonAssocSemiring.{v₁} A inst_1))) | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₂} B | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₂} B | |
| (@Semiring.toNonAssocSemiring.{v₂} B inst_3))) | |
| (@Algebra.toModule.{u, v₁} R A inst inst_1 inst_2) | |
| (@Algebra.toModule.{u, v₂} R B inst inst_3 inst_4)) | |
| (@TensorProduct.addCommMonoid.{u, v₁, v₂} R inst A B | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₁} A | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₁} A | |
| (@Semiring.toNonAssocSemiring.{v₁} A inst_1))) | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₂} B | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₂} B | |
| (@Semiring.toNonAssocSemiring.{v₂} B inst_3))) | |
| (@Algebra.toModule.{u, v₁} R A inst inst_1 inst_2) | |
| (@Algebra.toModule.{u, v₂} R B inst inst_3 inst_4)) | |
| (@TensorProduct.instModuleTensorProductToSemiringAddCommMonoid.{u, v₁, v₂} R inst A B | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₁} A | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₁} A | |
| (@Semiring.toNonAssocSemiring.{v₁} A inst_1))) | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₂} B | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₂} B | |
| (@Semiring.toNonAssocSemiring.{v₂} B inst_3))) | |
| (@Algebra.toModule.{u, v₁} R A inst inst_1 inst_2) | |
| (@Algebra.toModule.{u, v₂} R B inst inst_3 inst_4)) | |
| (@TensorProduct.instModuleTensorProductToSemiringAddCommMonoid.{u, v₁, v₂} R inst A B | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₁} A | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₁} A | |
| (@Semiring.toNonAssocSemiring.{v₁} A inst_1))) | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₂} B | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₂} B | |
| (@Semiring.toNonAssocSemiring.{v₂} B inst_3))) | |
| (@Algebra.toModule.{u, v₁} R A inst inst_1 inst_2) | |
| (@Algebra.toModule.{u, v₂} R B inst inst_3 inst_4))) | |
| a) | |
| (@LinearMap.instFunLikeLinearMap.{u, u, max v₂ v₁, max v₂ v₁} R R | |
| (@TensorProduct.{u, v₁, v₂} R inst A B | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₁} A | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₁} A (@Semiring.toNonAssocSemiring.{v₁} A inst_1))) | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₂} B | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₂} B (@Semiring.toNonAssocSemiring.{v₂} B inst_3))) | |
| (@Algebra.toModule.{u, v₁} R A inst inst_1 inst_2) (@Algebra.toModule.{u, v₂} R B inst inst_3 inst_4)) | |
| (@LinearMap.{u, u, max v₂ v₁, max v₂ v₁} R R (@CommSemiring.toSemiring.{u} R inst) | |
| (@CommSemiring.toSemiring.{u} R inst) | |
| (@RingHom.id.{u} R (@Semiring.toNonAssocSemiring.{u} R (@CommSemiring.toSemiring.{u} R inst))) | |
| (@TensorProduct.{u, v₁, v₂} R inst A B | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₁} A | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₁} A | |
| (@Semiring.toNonAssocSemiring.{v₁} A inst_1))) | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₂} B | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₂} B | |
| (@Semiring.toNonAssocSemiring.{v₂} B inst_3))) | |
| (@Algebra.toModule.{u, v₁} R A inst inst_1 inst_2) | |
| (@Algebra.toModule.{u, v₂} R B inst inst_3 inst_4)) | |
| (@TensorProduct.{u, v₁, v₂} R inst A B | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₁} A | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₁} A | |
| (@Semiring.toNonAssocSemiring.{v₁} A inst_1))) | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₂} B | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₂} B | |
| (@Semiring.toNonAssocSemiring.{v₂} B inst_3))) | |
| (@Algebra.toModule.{u, v₁} R A inst inst_1 inst_2) | |
| (@Algebra.toModule.{u, v₂} R B inst inst_3 inst_4)) | |
| (@TensorProduct.addCommMonoid.{u, v₁, v₂} R inst A B | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₁} A | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₁} A | |
| (@Semiring.toNonAssocSemiring.{v₁} A inst_1))) | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₂} B | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₂} B | |
| (@Semiring.toNonAssocSemiring.{v₂} B inst_3))) | |
| (@Algebra.toModule.{u, v₁} R A inst inst_1 inst_2) | |
| (@Algebra.toModule.{u, v₂} R B inst inst_3 inst_4)) | |
| (@TensorProduct.addCommMonoid.{u, v₁, v₂} R inst A B | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₁} A | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₁} A | |
| (@Semiring.toNonAssocSemiring.{v₁} A inst_1))) | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₂} B | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₂} B | |
| (@Semiring.toNonAssocSemiring.{v₂} B inst_3))) | |
| (@Algebra.toModule.{u, v₁} R A inst inst_1 inst_2) | |
| (@Algebra.toModule.{u, v₂} R B inst inst_3 inst_4)) | |
| (@TensorProduct.instModuleTensorProductToSemiringAddCommMonoid.{u, v₁, v₂} R inst A B | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₁} A | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₁} A | |
| (@Semiring.toNonAssocSemiring.{v₁} A inst_1))) | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₂} B | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₂} B | |
| (@Semiring.toNonAssocSemiring.{v₂} B inst_3))) | |
| (@Algebra.toModule.{u, v₁} R A inst inst_1 inst_2) | |
| (@Algebra.toModule.{u, v₂} R B inst inst_3 inst_4)) | |
| (@TensorProduct.instModuleTensorProductToSemiringAddCommMonoid.{u, v₁, v₂} R inst A B | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₁} A | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₁} A | |
| (@Semiring.toNonAssocSemiring.{v₁} A inst_1))) | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₂} B | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₂} B | |
| (@Semiring.toNonAssocSemiring.{v₂} B inst_3))) | |
| (@Algebra.toModule.{u, v₁} R A inst inst_1 inst_2) | |
| (@Algebra.toModule.{u, v₂} R B inst inst_3 inst_4))) | |
| (@CommSemiring.toSemiring.{u} R inst) (@CommSemiring.toSemiring.{u} R inst) | |
| (@TensorProduct.addCommMonoid.{u, v₁, v₂} R inst A B | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₁} A | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₁} A (@Semiring.toNonAssocSemiring.{v₁} A inst_1))) | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₂} B | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₂} B (@Semiring.toNonAssocSemiring.{v₂} B inst_3))) | |
| (@Algebra.toModule.{u, v₁} R A inst inst_1 inst_2) (@Algebra.toModule.{u, v₂} R B inst inst_3 inst_4)) | |
| (@LinearMap.addCommMonoid.{u, u, max v₁ v₂, max v₁ v₂} R R | |
| (@TensorProduct.{u, v₁, v₂} R inst A B | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₁} A | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₁} A | |
| (@Semiring.toNonAssocSemiring.{v₁} A inst_1))) | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₂} B | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₂} B | |
| (@Semiring.toNonAssocSemiring.{v₂} B inst_3))) | |
| (@Algebra.toModule.{u, v₁} R A inst inst_1 inst_2) | |
| (@Algebra.toModule.{u, v₂} R B inst inst_3 inst_4)) | |
| (@TensorProduct.{u, v₁, v₂} R inst A B | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₁} A | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₁} A | |
| (@Semiring.toNonAssocSemiring.{v₁} A inst_1))) | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₂} B | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₂} B | |
| (@Semiring.toNonAssocSemiring.{v₂} B inst_3))) | |
| (@Algebra.toModule.{u, v₁} R A inst inst_1 inst_2) | |
| (@Algebra.toModule.{u, v₂} R B inst inst_3 inst_4)) | |
| (@CommSemiring.toSemiring.{u} R inst) (@CommSemiring.toSemiring.{u} R inst) | |
| (@TensorProduct.addCommMonoid.{u, v₁, v₂} R inst A B | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₁} A | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₁} A | |
| (@Semiring.toNonAssocSemiring.{v₁} A inst_1))) | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₂} B | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₂} B | |
| (@Semiring.toNonAssocSemiring.{v₂} B inst_3))) | |
| (@Algebra.toModule.{u, v₁} R A inst inst_1 inst_2) | |
| (@Algebra.toModule.{u, v₂} R B inst inst_3 inst_4)) | |
| (@TensorProduct.addCommMonoid.{u, v₁, v₂} R inst A B | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₁} A | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₁} A | |
| (@Semiring.toNonAssocSemiring.{v₁} A inst_1))) | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₂} B | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₂} B | |
| (@Semiring.toNonAssocSemiring.{v₂} B inst_3))) | |
| (@Algebra.toModule.{u, v₁} R A inst inst_1 inst_2) | |
| (@Algebra.toModule.{u, v₂} R B inst inst_3 inst_4)) | |
| (@TensorProduct.instModuleTensorProductToSemiringAddCommMonoid.{u, v₁, v₂} R inst A B | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₁} A | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₁} A | |
| (@Semiring.toNonAssocSemiring.{v₁} A inst_1))) | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₂} B | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₂} B | |
| (@Semiring.toNonAssocSemiring.{v₂} B inst_3))) | |
| (@Algebra.toModule.{u, v₁} R A inst inst_1 inst_2) | |
| (@Algebra.toModule.{u, v₂} R B inst inst_3 inst_4)) | |
| (@TensorProduct.instModuleTensorProductToSemiringAddCommMonoid.{u, v₁, v₂} R inst A B | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₁} A | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₁} A | |
| (@Semiring.toNonAssocSemiring.{v₁} A inst_1))) | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₂} B | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₂} B | |
| (@Semiring.toNonAssocSemiring.{v₂} B inst_3))) | |
| (@Algebra.toModule.{u, v₁} R A inst inst_1 inst_2) | |
| (@Algebra.toModule.{u, v₂} R B inst inst_3 inst_4)) | |
| (@RingHom.id.{u} R (@Semiring.toNonAssocSemiring.{u} R (@CommSemiring.toSemiring.{u} R inst)))) | |
| (@TensorProduct.instModuleTensorProductToSemiringAddCommMonoid.{u, v₁, v₂} R inst A B | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₁} A | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₁} A (@Semiring.toNonAssocSemiring.{v₁} A inst_1))) | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₂} B | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₂} B (@Semiring.toNonAssocSemiring.{v₂} B inst_3))) | |
| (@Algebra.toModule.{u, v₁} R A inst inst_1 inst_2) (@Algebra.toModule.{u, v₂} R B inst inst_3 inst_4)) | |
| (@LinearMap.module.{u, u, u, max v₁ v₂, max v₁ v₂} R R R | |
| (@TensorProduct.{u, v₁, v₂} R inst A B | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₁} A | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₁} A | |
| (@Semiring.toNonAssocSemiring.{v₁} A inst_1))) | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₂} B | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₂} B | |
| (@Semiring.toNonAssocSemiring.{v₂} B inst_3))) | |
| (@Algebra.toModule.{u, v₁} R A inst inst_1 inst_2) | |
| (@Algebra.toModule.{u, v₂} R B inst inst_3 inst_4)) | |
| (@TensorProduct.{u, v₁, v₂} R inst A B | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₁} A | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₁} A | |
| (@Semiring.toNonAssocSemiring.{v₁} A inst_1))) | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₂} B | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₂} B | |
| (@Semiring.toNonAssocSemiring.{v₂} B inst_3))) | |
| (@Algebra.toModule.{u, v₁} R A inst inst_1 inst_2) | |
| (@Algebra.toModule.{u, v₂} R B inst inst_3 inst_4)) | |
| (@CommSemiring.toSemiring.{u} R inst) (@CommSemiring.toSemiring.{u} R inst) | |
| (@TensorProduct.addCommMonoid.{u, v₁, v₂} R inst A B | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₁} A | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₁} A | |
| (@Semiring.toNonAssocSemiring.{v₁} A inst_1))) | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₂} B | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₂} B | |
| (@Semiring.toNonAssocSemiring.{v₂} B inst_3))) | |
| (@Algebra.toModule.{u, v₁} R A inst inst_1 inst_2) | |
| (@Algebra.toModule.{u, v₂} R B inst inst_3 inst_4)) | |
| (@TensorProduct.addCommMonoid.{u, v₁, v₂} R inst A B | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₁} A | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₁} A | |
| (@Semiring.toNonAssocSemiring.{v₁} A inst_1))) | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₂} B | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₂} B | |
| (@Semiring.toNonAssocSemiring.{v₂} B inst_3))) | |
| (@Algebra.toModule.{u, v₁} R A inst inst_1 inst_2) | |
| (@Algebra.toModule.{u, v₂} R B inst inst_3 inst_4)) | |
| (@TensorProduct.instModuleTensorProductToSemiringAddCommMonoid.{u, v₁, v₂} R inst A B | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₁} A | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₁} A | |
| (@Semiring.toNonAssocSemiring.{v₁} A inst_1))) | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₂} B | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₂} B | |
| (@Semiring.toNonAssocSemiring.{v₂} B inst_3))) | |
| (@Algebra.toModule.{u, v₁} R A inst inst_1 inst_2) | |
| (@Algebra.toModule.{u, v₂} R B inst inst_3 inst_4)) | |
| (@TensorProduct.instModuleTensorProductToSemiringAddCommMonoid.{u, v₁, v₂} R inst A B | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₁} A | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₁} A | |
| (@Semiring.toNonAssocSemiring.{v₁} A inst_1))) | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₂} B | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₂} B | |
| (@Semiring.toNonAssocSemiring.{v₂} B inst_3))) | |
| (@Algebra.toModule.{u, v₁} R A inst inst_1 inst_2) | |
| (@Algebra.toModule.{u, v₂} R B inst inst_3 inst_4)) | |
| (@RingHom.id.{u} R (@Semiring.toNonAssocSemiring.{u} R (@CommSemiring.toSemiring.{u} R inst))) | |
| (@CommSemiring.toSemiring.{u} R inst) | |
| (@TensorProduct.instModuleTensorProductToSemiringAddCommMonoid.{u, v₁, v₂} R inst A B | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₁} A | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₁} A | |
| (@Semiring.toNonAssocSemiring.{v₁} A inst_1))) | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₂} B | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₂} B | |
| (@Semiring.toNonAssocSemiring.{v₂} B inst_3))) | |
| (@Algebra.toModule.{u, v₁} R A inst inst_1 inst_2) | |
| (@Algebra.toModule.{u, v₂} R B inst inst_3 inst_4)) | |
| (@Algebra.TensorProduct.instSemiring.proof_1.{u, v₁, v₂} R inst A inst_1 inst_2 B inst_3 inst_4)) | |
| (@RingHom.id.{u} R (@Semiring.toNonAssocSemiring.{u} R (@CommSemiring.toSemiring.{u} R inst)))) | |
| (@Algebra.TensorProduct.mul.{u, v₁, v₂} R inst A inst_1 inst_2 B inst_3 inst_4) a) | |
| b) | |
| (@Algebra.TensorProduct.instSemiring.proof_2.{u, v₁, v₂} R inst A inst_1 inst_2 B inst_3 inst_4) | |
| (@Algebra.TensorProduct.instSemiring.proof_3.{u, v₁, v₂} R inst A inst_1 inst_2 B inst_3 inst_4) | |
| (@Algebra.TensorProduct.instSemiring.proof_4.{u, v₁, v₂} R inst A inst_1 inst_2 B inst_3 inst_4) | |
| (@Algebra.TensorProduct.instSemiring.proof_5.{u, v₁, v₂} R inst A inst_1 inst_2 B inst_3 inst_4)) | |
| (@Algebra.TensorProduct.mul_assoc.{u, v₁, v₂} R inst A inst_1 inst_2 B inst_3 inst_4)) | |
| (@Algebra.TensorProduct.instOneTensorProductToAddCommMonoidToNonUnitalNonAssocSemiringToNonAssocSemiringToAddCommMonoidToNonUnitalNonAssocSemiringToNonAssocSemiringToModuleToModule.{u, | |
| v₁, v₂} | |
| R inst A inst_1 inst_2 B inst_3 inst_4) | |
| (@Algebra.TensorProduct.one_mul.{u, v₁, v₂} R inst A inst_1 inst_2 B inst_3 inst_4) | |
| (@Algebra.TensorProduct.mul_one.{u, v₁, v₂} R inst A inst_1 inst_2 B inst_3 inst_4) | |
| (@AddMonoidWithOne.toNatCast.{max v₁ v₂} | |
| (@TensorProduct.{u, v₁, v₂} R inst A B | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₁} A | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₁} A (@Semiring.toNonAssocSemiring.{v₁} A inst_1))) | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₂} B | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₂} B (@Semiring.toNonAssocSemiring.{v₂} B inst_3))) | |
| (@Algebra.toModule.{u, v₁} R A inst inst_1 inst_2) (@Algebra.toModule.{u, v₂} R B inst inst_3 inst_4)) | |
| (@Algebra.TensorProduct.instAddMonoidWithOneTensorProductToAddCommMonoidToNonUnitalNonAssocSemiringToNonAssocSemiringToAddCommMonoidToNonUnitalNonAssocSemiringToNonAssocSemiringToModuleToModule.{u, | |
| v₁, v₂} | |
| R inst A inst_1 inst_2 B inst_3 inst_4)) | |
| (@Algebra.TensorProduct.instSemiring.proof_6.{v₁, v₂, u} R inst A inst_1 inst_2 B inst_3 inst_4) | |
| (@Algebra.TensorProduct.instSemiring.proof_7.{v₁, v₂, u} R inst A inst_1 inst_2 B inst_3 inst_4) | |
| (@npowRec.{max v₁ v₂} | |
| (@TensorProduct.{u, v₁, v₂} R inst A B | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₁} A | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₁} A (@Semiring.toNonAssocSemiring.{v₁} A inst_1))) | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₂} B | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₂} B (@Semiring.toNonAssocSemiring.{v₂} B inst_3))) | |
| (@Algebra.toModule.{u, v₁} R A inst inst_1 inst_2) (@Algebra.toModule.{u, v₂} R B inst inst_3 inst_4)) | |
| (@Algebra.TensorProduct.instOneTensorProductToAddCommMonoidToNonUnitalNonAssocSemiringToNonAssocSemiringToAddCommMonoidToNonUnitalNonAssocSemiringToNonAssocSemiringToModuleToModule.{u, | |
| v₁, v₂} | |
| R inst A inst_1 inst_2 B inst_3 inst_4) | |
| (@NonUnitalNonAssocSemiring.toMul.{max v₁ v₂} | |
| (@TensorProduct.{u, v₁, v₂} R inst A B | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₁} A | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₁} A (@Semiring.toNonAssocSemiring.{v₁} A inst_1))) | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₂} B | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₂} B (@Semiring.toNonAssocSemiring.{v₂} B inst_3))) | |
| (@Algebra.toModule.{u, v₁} R A inst inst_1 inst_2) (@Algebra.toModule.{u, v₂} R B inst inst_3 inst_4)) | |
| (@NonUnitalSemiring.toNonUnitalNonAssocSemiring.{max v₁ v₂} | |
| (@TensorProduct.{u, v₁, v₂} R inst A B | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₁} A | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₁} A (@Semiring.toNonAssocSemiring.{v₁} A inst_1))) | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₂} B | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₂} B (@Semiring.toNonAssocSemiring.{v₂} B inst_3))) | |
| (@Algebra.toModule.{u, v₁} R A inst inst_1 inst_2) (@Algebra.toModule.{u, v₂} R B inst inst_3 inst_4)) | |
| (@NonUnitalSemiring.mk.{max v₁ v₂} | |
| (@TensorProduct.{u, v₁, v₂} R inst A B | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₁} A | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₁} A (@Semiring.toNonAssocSemiring.{v₁} A inst_1))) | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₂} B | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₂} B (@Semiring.toNonAssocSemiring.{v₂} B inst_3))) | |
| (@Algebra.toModule.{u, v₁} R A inst inst_1 inst_2) (@Algebra.toModule.{u, v₂} R B inst inst_3 inst_4)) | |
| (@NonUnitalNonAssocSemiring.mk.{max v₁ v₂} | |
| (@TensorProduct.{u, v₁, v₂} R inst A B | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₁} A | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₁} A (@Semiring.toNonAssocSemiring.{v₁} A inst_1))) | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₂} B | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₂} B (@Semiring.toNonAssocSemiring.{v₂} B inst_3))) | |
| (@Algebra.toModule.{u, v₁} R A inst inst_1 inst_2) (@Algebra.toModule.{u, v₂} R B inst inst_3 inst_4)) | |
| (@inferInstance.{max (v₁ + 1) (v₂ + 1)} | |
| (AddCommMonoid.{max v₁ v₂} | |
| (@TensorProduct.{u, v₁, v₂} R inst A B | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₁} A | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₁} A | |
| (@Semiring.toNonAssocSemiring.{v₁} A inst_1))) | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₂} B | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₂} B | |
| (@Semiring.toNonAssocSemiring.{v₂} B inst_3))) | |
| (@Algebra.toModule.{u, v₁} R A inst inst_1 inst_2) | |
| (@Algebra.toModule.{u, v₂} R B inst inst_3 inst_4))) | |
| (@Algebra.TensorProduct.instAddCommMonoidTensorProductToAddCommMonoidToNonUnitalNonAssocSemiringToNonAssocSemiringToAddCommMonoidToNonUnitalNonAssocSemiringToNonAssocSemiringToModuleToModule.{u, | |
| v₁, v₂} | |
| R inst A inst_1 inst_2 B inst_3 inst_4)) | |
| (@Mul.mk.{max v₁ v₂} | |
| (@TensorProduct.{u, v₁, v₂} R inst A B | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₁} A | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₁} A (@Semiring.toNonAssocSemiring.{v₁} A inst_1))) | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₂} B | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₂} B (@Semiring.toNonAssocSemiring.{v₂} B inst_3))) | |
| (@Algebra.toModule.{u, v₁} R A inst inst_1 inst_2) (@Algebra.toModule.{u, v₂} R B inst inst_3 inst_4)) | |
| fun | |
| (a b : | |
| @TensorProduct.{u, v₁, v₂} R inst A B | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₁} A | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₁} A | |
| (@Semiring.toNonAssocSemiring.{v₁} A inst_1))) | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₂} B | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₂} B | |
| (@Semiring.toNonAssocSemiring.{v₂} B inst_3))) | |
| (@Algebra.toModule.{u, v₁} R A inst inst_1 inst_2) | |
| (@Algebra.toModule.{u, v₂} R B inst inst_3 inst_4)) ↦ | |
| @FunLike.coe.{max (v₁ + 1) (v₂ + 1), max (v₁ + 1) (v₂ + 1), max (v₁ + 1) (v₂ + 1)} | |
| (@LinearMap.{u, u, max v₂ v₁, max v₂ v₁} R R (@CommSemiring.toSemiring.{u} R inst) | |
| (@CommSemiring.toSemiring.{u} R inst) | |
| (@RingHom.id.{u} R (@Semiring.toNonAssocSemiring.{u} R (@CommSemiring.toSemiring.{u} R inst))) | |
| (@TensorProduct.{u, v₁, v₂} R inst A B | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₁} A | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₁} A | |
| (@Semiring.toNonAssocSemiring.{v₁} A inst_1))) | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₂} B | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₂} B | |
| (@Semiring.toNonAssocSemiring.{v₂} B inst_3))) | |
| (@Algebra.toModule.{u, v₁} R A inst inst_1 inst_2) | |
| (@Algebra.toModule.{u, v₂} R B inst inst_3 inst_4)) | |
| (@TensorProduct.{u, v₁, v₂} R inst A B | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₁} A | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₁} A | |
| (@Semiring.toNonAssocSemiring.{v₁} A inst_1))) | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₂} B | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₂} B | |
| (@Semiring.toNonAssocSemiring.{v₂} B inst_3))) | |
| (@Algebra.toModule.{u, v₁} R A inst inst_1 inst_2) | |
| (@Algebra.toModule.{u, v₂} R B inst inst_3 inst_4)) | |
| (@TensorProduct.addCommMonoid.{u, v₁, v₂} R inst A B | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₁} A | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₁} A | |
| (@Semiring.toNonAssocSemiring.{v₁} A inst_1))) | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₂} B | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₂} B | |
| (@Semiring.toNonAssocSemiring.{v₂} B inst_3))) | |
| (@Algebra.toModule.{u, v₁} R A inst inst_1 inst_2) | |
| (@Algebra.toModule.{u, v₂} R B inst inst_3 inst_4)) | |
| (@TensorProduct.addCommMonoid.{u, v₁, v₂} R inst A B | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₁} A | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₁} A | |
| (@Semiring.toNonAssocSemiring.{v₁} A inst_1))) | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₂} B | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₂} B | |
| (@Semiring.toNonAssocSemiring.{v₂} B inst_3))) | |
| (@Algebra.toModule.{u, v₁} R A inst inst_1 inst_2) | |
| (@Algebra.toModule.{u, v₂} R B inst inst_3 inst_4)) | |
| (@TensorProduct.instModuleTensorProductToSemiringAddCommMonoid.{u, v₁, v₂} R inst A B | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₁} A | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₁} A | |
| (@Semiring.toNonAssocSemiring.{v₁} A inst_1))) | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₂} B | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₂} B | |
| (@Semiring.toNonAssocSemiring.{v₂} B inst_3))) | |
| (@Algebra.toModule.{u, v₁} R A inst inst_1 inst_2) | |
| (@Algebra.toModule.{u, v₂} R B inst inst_3 inst_4)) | |
| (@TensorProduct.instModuleTensorProductToSemiringAddCommMonoid.{u, v₁, v₂} R inst A B | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₁} A | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₁} A | |
| (@Semiring.toNonAssocSemiring.{v₁} A inst_1))) | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₂} B | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₂} B | |
| (@Semiring.toNonAssocSemiring.{v₂} B inst_3))) | |
| (@Algebra.toModule.{u, v₁} R A inst inst_1 inst_2) | |
| (@Algebra.toModule.{u, v₂} R B inst inst_3 inst_4))) | |
| (@TensorProduct.{u, v₁, v₂} R inst A B | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₁} A | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₁} A | |
| (@Semiring.toNonAssocSemiring.{v₁} A inst_1))) | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₂} B | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₂} B | |
| (@Semiring.toNonAssocSemiring.{v₂} B inst_3))) | |
| (@Algebra.toModule.{u, v₁} R A inst inst_1 inst_2) | |
| (@Algebra.toModule.{u, v₂} R B inst inst_3 inst_4)) | |
| (fun | |
| (a : | |
| @TensorProduct.{u, v₁, v₂} R inst A B | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₁} A | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₁} A | |
| (@Semiring.toNonAssocSemiring.{v₁} A inst_1))) | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₂} B | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₂} B | |
| (@Semiring.toNonAssocSemiring.{v₂} B inst_3))) | |
| (@Algebra.toModule.{u, v₁} R A inst inst_1 inst_2) | |
| (@Algebra.toModule.{u, v₂} R B inst inst_3 inst_4)) ↦ | |
| @TensorProduct.{u, v₁, v₂} R inst A B | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₁} A | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₁} A | |
| (@Semiring.toNonAssocSemiring.{v₁} A inst_1))) | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₂} B | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₂} B | |
| (@Semiring.toNonAssocSemiring.{v₂} B inst_3))) | |
| (@Algebra.toModule.{u, v₁} R A inst inst_1 inst_2) | |
| (@Algebra.toModule.{u, v₂} R B inst inst_3 inst_4)) | |
| (@LinearMap.instFunLikeLinearMap.{u, u, max v₁ v₂, max v₁ v₂} R R | |
| (@TensorProduct.{u, v₁, v₂} R inst A B | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₁} A | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₁} A | |
| (@Semiring.toNonAssocSemiring.{v₁} A inst_1))) | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₂} B | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₂} B | |
| (@Semiring.toNonAssocSemiring.{v₂} B inst_3))) | |
| (@Algebra.toModule.{u, v₁} R A inst inst_1 inst_2) | |
| (@Algebra.toModule.{u, v₂} R B inst inst_3 inst_4)) | |
| (@TensorProduct.{u, v₁, v₂} R inst A B | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₁} A | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₁} A | |
| (@Semiring.toNonAssocSemiring.{v₁} A inst_1))) | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₂} B | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₂} B | |
| (@Semiring.toNonAssocSemiring.{v₂} B inst_3))) | |
| (@Algebra.toModule.{u, v₁} R A inst inst_1 inst_2) | |
| (@Algebra.toModule.{u, v₂} R B inst inst_3 inst_4)) | |
| (@CommSemiring.toSemiring.{u} R inst) (@CommSemiring.toSemiring.{u} R inst) | |
| (@TensorProduct.addCommMonoid.{u, v₁, v₂} R inst A B | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₁} A | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₁} A | |
| (@Semiring.toNonAssocSemiring.{v₁} A inst_1))) | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₂} B | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₂} B | |
| (@Semiring.toNonAssocSemiring.{v₂} B inst_3))) | |
| (@Algebra.toModule.{u, v₁} R A inst inst_1 inst_2) | |
| (@Algebra.toModule.{u, v₂} R B inst inst_3 inst_4)) | |
| (@TensorProduct.addCommMonoid.{u, v₁, v₂} R inst A B | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₁} A | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₁} A | |
| (@Semiring.toNonAssocSemiring.{v₁} A inst_1))) | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₂} B | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₂} B | |
| (@Semiring.toNonAssocSemiring.{v₂} B inst_3))) | |
| (@Algebra.toModule.{u, v₁} R A inst inst_1 inst_2) | |
| (@Algebra.toModule.{u, v₂} R B inst inst_3 inst_4)) | |
| (@TensorProduct.instModuleTensorProductToSemiringAddCommMonoid.{u, v₁, v₂} R inst A B | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₁} A | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₁} A | |
| (@Semiring.toNonAssocSemiring.{v₁} A inst_1))) | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₂} B | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₂} B | |
| (@Semiring.toNonAssocSemiring.{v₂} B inst_3))) | |
| (@Algebra.toModule.{u, v₁} R A inst inst_1 inst_2) | |
| (@Algebra.toModule.{u, v₂} R B inst inst_3 inst_4)) | |
| (@TensorProduct.instModuleTensorProductToSemiringAddCommMonoid.{u, v₁, v₂} R inst A B | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₁} A | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₁} A | |
| (@Semiring.toNonAssocSemiring.{v₁} A inst_1))) | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₂} B | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₂} B | |
| (@Semiring.toNonAssocSemiring.{v₂} B inst_3))) | |
| (@Algebra.toModule.{u, v₁} R A inst inst_1 inst_2) | |
| (@Algebra.toModule.{u, v₂} R B inst inst_3 inst_4)) | |
| (@RingHom.id.{u} R (@Semiring.toNonAssocSemiring.{u} R (@CommSemiring.toSemiring.{u} R inst)))) | |
| (@FunLike.coe.{max (v₂ + 1) (v₁ + 1), max (v₂ + 1) (v₁ + 1), max (v₂ + 1) (v₁ + 1)} | |
| (@LinearMap.{u, u, max v₂ v₁, max v₂ v₁} R R (@CommSemiring.toSemiring.{u} R inst) | |
| (@CommSemiring.toSemiring.{u} R inst) | |
| (@RingHom.id.{u} R (@Semiring.toNonAssocSemiring.{u} R (@CommSemiring.toSemiring.{u} R inst))) | |
| (@TensorProduct.{u, v₁, v₂} R inst A B | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₁} A | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₁} A | |
| (@Semiring.toNonAssocSemiring.{v₁} A inst_1))) | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₂} B | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₂} B | |
| (@Semiring.toNonAssocSemiring.{v₂} B inst_3))) | |
| (@Algebra.toModule.{u, v₁} R A inst inst_1 inst_2) | |
| (@Algebra.toModule.{u, v₂} R B inst inst_3 inst_4)) | |
| (@LinearMap.{u, u, max v₂ v₁, max v₂ v₁} R R (@CommSemiring.toSemiring.{u} R inst) | |
| (@CommSemiring.toSemiring.{u} R inst) | |
| (@RingHom.id.{u} R (@Semiring.toNonAssocSemiring.{u} R (@CommSemiring.toSemiring.{u} R inst))) | |
| (@TensorProduct.{u, v₁, v₂} R inst A B | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₁} A | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₁} A | |
| (@Semiring.toNonAssocSemiring.{v₁} A inst_1))) | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₂} B | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₂} B | |
| (@Semiring.toNonAssocSemiring.{v₂} B inst_3))) | |
| (@Algebra.toModule.{u, v₁} R A inst inst_1 inst_2) | |
| (@Algebra.toModule.{u, v₂} R B inst inst_3 inst_4)) | |
| (@TensorProduct.{u, v₁, v₂} R inst A B | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₁} A | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₁} A | |
| (@Semiring.toNonAssocSemiring.{v₁} A inst_1))) | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₂} B | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₂} B | |
| (@Semiring.toNonAssocSemiring.{v₂} B inst_3))) | |
| (@Algebra.toModule.{u, v₁} R A inst inst_1 inst_2) | |
| (@Algebra.toModule.{u, v₂} R B inst inst_3 inst_4)) | |
| (@TensorProduct.addCommMonoid.{u, v₁, v₂} R inst A B | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₁} A | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₁} A | |
| (@Semiring.toNonAssocSemiring.{v₁} A inst_1))) | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₂} B | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₂} B | |
| (@Semiring.toNonAssocSemiring.{v₂} B inst_3))) | |
| (@Algebra.toModule.{u, v₁} R A inst inst_1 inst_2) | |
| (@Algebra.toModule.{u, v₂} R B inst inst_3 inst_4)) | |
| (@TensorProduct.addCommMonoid.{u, v₁, v₂} R inst A B | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₁} A | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₁} A | |
| (@Semiring.toNonAssocSemiring.{v₁} A inst_1))) | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₂} B | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₂} B | |
| (@Semiring.toNonAssocSemiring.{v₂} B inst_3))) | |
| (@Algebra.toModule.{u, v₁} R A inst inst_1 inst_2) | |
| (@Algebra.toModule.{u, v₂} R B inst inst_3 inst_4)) | |
| (@TensorProduct.instModuleTensorProductToSemiringAddCommMonoid.{u, v₁, v₂} R inst A B | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₁} A | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₁} A | |
| (@Semiring.toNonAssocSemiring.{v₁} A inst_1))) | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₂} B | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₂} B | |
| (@Semiring.toNonAssocSemiring.{v₂} B inst_3))) | |
| (@Algebra.toModule.{u, v₁} R A inst inst_1 inst_2) | |
| (@Algebra.toModule.{u, v₂} R B inst inst_3 inst_4)) | |
| (@TensorProduct.instModuleTensorProductToSemiringAddCommMonoid.{u, v₁, v₂} R inst A B | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₁} A | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₁} A | |
| (@Semiring.toNonAssocSemiring.{v₁} A inst_1))) | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₂} B | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₂} B | |
| (@Semiring.toNonAssocSemiring.{v₂} B inst_3))) | |
| (@Algebra.toModule.{u, v₁} R A inst inst_1 inst_2) | |
| (@Algebra.toModule.{u, v₂} R B inst inst_3 inst_4))) | |
| (@TensorProduct.addCommMonoid.{u, v₁, v₂} R inst A B | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₁} A | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₁} A | |
| (@Semiring.toNonAssocSemiring.{v₁} A inst_1))) | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₂} B | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₂} B | |
| (@Semiring.toNonAssocSemiring.{v₂} B inst_3))) | |
| (@Algebra.toModule.{u, v₁} R A inst inst_1 inst_2) | |
| (@Algebra.toModule.{u, v₂} R B inst inst_3 inst_4)) | |
| (@LinearMap.addCommMonoid.{u, u, max v₁ v₂, max v₁ v₂} R R | |
| (@TensorProduct.{u, v₁, v₂} R inst A B | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₁} A | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₁} A | |
| (@Semiring.toNonAssocSemiring.{v₁} A inst_1))) | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₂} B | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₂} B | |
| (@Semiring.toNonAssocSemiring.{v₂} B inst_3))) | |
| (@Algebra.toModule.{u, v₁} R A inst inst_1 inst_2) | |
| (@Algebra.toModule.{u, v₂} R B inst inst_3 inst_4)) | |
| (@TensorProduct.{u, v₁, v₂} R inst A B | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₁} A | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₁} A | |
| (@Semiring.toNonAssocSemiring.{v₁} A inst_1))) | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₂} B | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₂} B | |
| (@Semiring.toNonAssocSemiring.{v₂} B inst_3))) | |
| (@Algebra.toModule.{u, v₁} R A inst inst_1 inst_2) | |
| (@Algebra.toModule.{u, v₂} R B inst inst_3 inst_4)) | |
| (@CommSemiring.toSemiring.{u} R inst) (@CommSemiring.toSemiring.{u} R inst) | |
| (@TensorProduct.addCommMonoid.{u, v₁, v₂} R inst A B | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₁} A | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₁} A | |
| (@Semiring.toNonAssocSemiring.{v₁} A inst_1))) | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₂} B | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₂} B | |
| (@Semiring.toNonAssocSemiring.{v₂} B inst_3))) | |
| (@Algebra.toModule.{u, v₁} R A inst inst_1 inst_2) | |
| (@Algebra.toModule.{u, v₂} R B inst inst_3 inst_4)) | |
| (@TensorProduct.addCommMonoid.{u, v₁, v₂} R inst A B | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₁} A | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₁} A | |
| (@Semiring.toNonAssocSemiring.{v₁} A inst_1))) | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₂} B | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₂} B | |
| (@Semiring.toNonAssocSemiring.{v₂} B inst_3))) | |
| (@Algebra.toModule.{u, v₁} R A inst inst_1 inst_2) | |
| (@Algebra.toModule.{u, v₂} R B inst inst_3 inst_4)) | |
| (@TensorProduct.instModuleTensorProductToSemiringAddCommMonoid.{u, v₁, v₂} R inst A B | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₁} A | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₁} A | |
| (@Semiring.toNonAssocSemiring.{v₁} A inst_1))) | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₂} B | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₂} B | |
| (@Semiring.toNonAssocSemiring.{v₂} B inst_3))) | |
| (@Algebra.toModule.{u, v₁} R A inst inst_1 inst_2) | |
| (@Algebra.toModule.{u, v₂} R B inst inst_3 inst_4)) | |
| (@TensorProduct.instModuleTensorProductToSemiringAddCommMonoid.{u, v₁, v₂} R inst A B | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₁} A | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₁} A | |
| (@Semiring.toNonAssocSemiring.{v₁} A inst_1))) | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₂} B | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₂} B | |
| (@Semiring.toNonAssocSemiring.{v₂} B inst_3))) | |
| (@Algebra.toModule.{u, v₁} R A inst inst_1 inst_2) | |
| (@Algebra.toModule.{u, v₂} R B inst inst_3 inst_4)) | |
| (@RingHom.id.{u} R (@Semiring.toNonAssocSemiring.{u} R (@CommSemiring.toSemiring.{u} R inst)))) | |
| (@TensorProduct.instModuleTensorProductToSemiringAddCommMonoid.{u, v₁, v₂} R inst A B | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₁} A | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₁} A | |
| (@Semiring.toNonAssocSemiring.{v₁} A inst_1))) | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₂} B | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₂} B | |
| (@Semiring.toNonAssocSemiring.{v₂} B inst_3))) | |
| (@Algebra.toModule.{u, v₁} R A inst inst_1 inst_2) | |
| (@Algebra.toModule.{u, v₂} R B inst inst_3 inst_4)) | |
| (@LinearMap.module.{u, u, u, max v₁ v₂, max v₁ v₂} R R R | |
| (@TensorProduct.{u, v₁, v₂} R inst A B | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₁} A | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₁} A | |
| (@Semiring.toNonAssocSemiring.{v₁} A inst_1))) | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₂} B | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₂} B | |
| (@Semiring.toNonAssocSemiring.{v₂} B inst_3))) | |
| (@Algebra.toModule.{u, v₁} R A inst inst_1 inst_2) | |
| (@Algebra.toModule.{u, v₂} R B inst inst_3 inst_4)) | |
| (@TensorProduct.{u, v₁, v₂} R inst A B | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₁} A | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₁} A | |
| (@Semiring.toNonAssocSemiring.{v₁} A inst_1))) | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₂} B | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₂} B | |
| (@Semiring.toNonAssocSemiring.{v₂} B inst_3))) | |
| (@Algebra.toModule.{u, v₁} R A inst inst_1 inst_2) | |
| (@Algebra.toModule.{u, v₂} R B inst inst_3 inst_4)) | |
| (@CommSemiring.toSemiring.{u} R inst) (@CommSemiring.toSemiring.{u} R inst) | |
| (@TensorProduct.addCommMonoid.{u, v₁, v₂} R inst A B | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₁} A | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₁} A | |
| (@Semiring.toNonAssocSemiring.{v₁} A inst_1))) | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₂} B | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₂} B | |
| (@Semiring.toNonAssocSemiring.{v₂} B inst_3))) | |
| (@Algebra.toModule.{u, v₁} R A inst inst_1 inst_2) | |
| (@Algebra.toModule.{u, v₂} R B inst inst_3 inst_4)) | |
| (@TensorProduct.addCommMonoid.{u, v₁, v₂} R inst A B | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₁} A | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₁} A | |
| (@Semiring.toNonAssocSemiring.{v₁} A inst_1))) | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₂} B | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₂} B | |
| (@Semiring.toNonAssocSemiring.{v₂} B inst_3))) | |
| (@Algebra.toModule.{u, v₁} R A inst inst_1 inst_2) | |
| (@Algebra.toModule.{u, v₂} R B inst inst_3 inst_4)) | |
| (@TensorProduct.instModuleTensorProductToSemiringAddCommMonoid.{u, v₁, v₂} R inst A B | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₁} A | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₁} A | |
| (@Semiring.toNonAssocSemiring.{v₁} A inst_1))) | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₂} B | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₂} B | |
| (@Semiring.toNonAssocSemiring.{v₂} B inst_3))) | |
| (@Algebra.toModule.{u, v₁} R A inst inst_1 inst_2) | |
| (@Algebra.toModule.{u, v₂} R B inst inst_3 inst_4)) | |
| (@TensorProduct.instModuleTensorProductToSemiringAddCommMonoid.{u, v₁, v₂} R inst A B | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₁} A | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₁} A | |
| (@Semiring.toNonAssocSemiring.{v₁} A inst_1))) | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₂} B | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₂} B | |
| (@Semiring.toNonAssocSemiring.{v₂} B inst_3))) | |
| (@Algebra.toModule.{u, v₁} R A inst inst_1 inst_2) | |
| (@Algebra.toModule.{u, v₂} R B inst inst_3 inst_4)) | |
| (@RingHom.id.{u} R (@Semiring.toNonAssocSemiring.{u} R (@CommSemiring.toSemiring.{u} R inst))) | |
| (@CommSemiring.toSemiring.{u} R inst) | |
| (@TensorProduct.instModuleTensorProductToSemiringAddCommMonoid.{u, v₁, v₂} R inst A B | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₁} A | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₁} A | |
| (@Semiring.toNonAssocSemiring.{v₁} A inst_1))) | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₂} B | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₂} B | |
| (@Semiring.toNonAssocSemiring.{v₂} B inst_3))) | |
| (@Algebra.toModule.{u, v₁} R A inst inst_1 inst_2) | |
| (@Algebra.toModule.{u, v₂} R B inst inst_3 inst_4)) | |
| (@Algebra.TensorProduct.instSemiring.proof_1.{u, v₁, v₂} R inst A inst_1 inst_2 B inst_3 | |
| inst_4))) | |
| (@TensorProduct.{u, v₁, v₂} R inst A B | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₁} A | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₁} A | |
| (@Semiring.toNonAssocSemiring.{v₁} A inst_1))) | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₂} B | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₂} B | |
| (@Semiring.toNonAssocSemiring.{v₂} B inst_3))) | |
| (@Algebra.toModule.{u, v₁} R A inst inst_1 inst_2) | |
| (@Algebra.toModule.{u, v₂} R B inst inst_3 inst_4)) | |
| (fun | |
| (a : | |
| @TensorProduct.{u, v₁, v₂} R inst A B | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₁} A | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₁} A | |
| (@Semiring.toNonAssocSemiring.{v₁} A inst_1))) | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₂} B | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₂} B | |
| (@Semiring.toNonAssocSemiring.{v₂} B inst_3))) | |
| (@Algebra.toModule.{u, v₁} R A inst inst_1 inst_2) | |
| (@Algebra.toModule.{u, v₂} R B inst inst_3 inst_4)) ↦ | |
| @LinearMap.{u, u, max v₂ v₁, max v₂ v₁} R R (@CommSemiring.toSemiring.{u} R inst) | |
| (@CommSemiring.toSemiring.{u} R inst) | |
| (@RingHom.id.{u} R (@Semiring.toNonAssocSemiring.{u} R (@CommSemiring.toSemiring.{u} R inst))) | |
| (@TensorProduct.{u, v₁, v₂} R inst A B | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₁} A | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₁} A | |
| (@Semiring.toNonAssocSemiring.{v₁} A inst_1))) | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₂} B | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₂} B | |
| (@Semiring.toNonAssocSemiring.{v₂} B inst_3))) | |
| (@Algebra.toModule.{u, v₁} R A inst inst_1 inst_2) | |
| (@Algebra.toModule.{u, v₂} R B inst inst_3 inst_4)) | |
| (@TensorProduct.{u, v₁, v₂} R inst A B | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₁} A | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₁} A | |
| (@Semiring.toNonAssocSemiring.{v₁} A inst_1))) | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₂} B | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₂} B | |
| (@Semiring.toNonAssocSemiring.{v₂} B inst_3))) | |
| (@Algebra.toModule.{u, v₁} R A inst inst_1 inst_2) | |
| (@Algebra.toModule.{u, v₂} R B inst inst_3 inst_4)) | |
| (@TensorProduct.addCommMonoid.{u, v₁, v₂} R inst A B | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₁} A | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₁} A | |
| (@Semiring.toNonAssocSemiring.{v₁} A inst_1))) | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₂} B | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₂} B | |
| (@Semiring.toNonAssocSemiring.{v₂} B inst_3))) | |
| (@Algebra.toModule.{u, v₁} R A inst inst_1 inst_2) | |
| (@Algebra.toModule.{u, v₂} R B inst inst_3 inst_4)) | |
| (@TensorProduct.addCommMonoid.{u, v₁, v₂} R inst A B | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₁} A | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₁} A | |
| (@Semiring.toNonAssocSemiring.{v₁} A inst_1))) | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₂} B | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₂} B | |
| (@Semiring.toNonAssocSemiring.{v₂} B inst_3))) | |
| (@Algebra.toModule.{u, v₁} R A inst inst_1 inst_2) | |
| (@Algebra.toModule.{u, v₂} R B inst inst_3 inst_4)) | |
| (@TensorProduct.instModuleTensorProductToSemiringAddCommMonoid.{u, v₁, v₂} R inst A B | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₁} A | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₁} A | |
| (@Semiring.toNonAssocSemiring.{v₁} A inst_1))) | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₂} B | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₂} B | |
| (@Semiring.toNonAssocSemiring.{v₂} B inst_3))) | |
| (@Algebra.toModule.{u, v₁} R A inst inst_1 inst_2) | |
| (@Algebra.toModule.{u, v₂} R B inst inst_3 inst_4)) | |
| (@TensorProduct.instModuleTensorProductToSemiringAddCommMonoid.{u, v₁, v₂} R inst A B | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₁} A | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₁} A | |
| (@Semiring.toNonAssocSemiring.{v₁} A inst_1))) | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₂} B | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₂} B | |
| (@Semiring.toNonAssocSemiring.{v₂} B inst_3))) | |
| (@Algebra.toModule.{u, v₁} R A inst inst_1 inst_2) | |
| (@Algebra.toModule.{u, v₂} R B inst inst_3 inst_4))) | |
| (@LinearMap.instFunLikeLinearMap.{u, u, max v₂ v₁, max v₂ v₁} R R | |
| (@TensorProduct.{u, v₁, v₂} R inst A B | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₁} A | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₁} A | |
| (@Semiring.toNonAssocSemiring.{v₁} A inst_1))) | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₂} B | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₂} B | |
| (@Semiring.toNonAssocSemiring.{v₂} B inst_3))) | |
| (@Algebra.toModule.{u, v₁} R A inst inst_1 inst_2) | |
| (@Algebra.toModule.{u, v₂} R B inst inst_3 inst_4)) | |
| (@LinearMap.{u, u, max v₂ v₁, max v₂ v₁} R R (@CommSemiring.toSemiring.{u} R inst) | |
| (@CommSemiring.toSemiring.{u} R inst) | |
| (@RingHom.id.{u} R (@Semiring.toNonAssocSemiring.{u} R (@CommSemiring.toSemiring.{u} R inst))) | |
| (@TensorProduct.{u, v₁, v₂} R inst A B | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₁} A | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₁} A | |
| (@Semiring.toNonAssocSemiring.{v₁} A inst_1))) | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₂} B | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₂} B | |
| (@Semiring.toNonAssocSemiring.{v₂} B inst_3))) | |
| (@Algebra.toModule.{u, v₁} R A inst inst_1 inst_2) | |
| (@Algebra.toModule.{u, v₂} R B inst inst_3 inst_4)) | |
| (@TensorProduct.{u, v₁, v₂} R inst A B | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₁} A | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₁} A | |
| (@Semiring.toNonAssocSemiring.{v₁} A inst_1))) | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₂} B | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₂} B | |
| (@Semiring.toNonAssocSemiring.{v₂} B inst_3))) | |
| (@Algebra.toModule.{u, v₁} R A inst inst_1 inst_2) | |
| (@Algebra.toModule.{u, v₂} R B inst inst_3 inst_4)) | |
| (@TensorProduct.addCommMonoid.{u, v₁, v₂} R inst A B | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₁} A | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₁} A | |
| (@Semiring.toNonAssocSemiring.{v₁} A inst_1))) | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₂} B | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₂} B | |
| (@Semiring.toNonAssocSemiring.{v₂} B inst_3))) | |
| (@Algebra.toModule.{u, v₁} R A inst inst_1 inst_2) | |
| (@Algebra.toModule.{u, v₂} R B inst inst_3 inst_4)) | |
| (@TensorProduct.addCommMonoid.{u, v₁, v₂} R inst A B | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₁} A | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₁} A | |
| (@Semiring.toNonAssocSemiring.{v₁} A inst_1))) | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₂} B | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₂} B | |
| (@Semiring.toNonAssocSemiring.{v₂} B inst_3))) | |
| (@Algebra.toModule.{u, v₁} R A inst inst_1 inst_2) | |
| (@Algebra.toModule.{u, v₂} R B inst inst_3 inst_4)) | |
| (@TensorProduct.instModuleTensorProductToSemiringAddCommMonoid.{u, v₁, v₂} R inst A B | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₁} A | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₁} A | |
| (@Semiring.toNonAssocSemiring.{v₁} A inst_1))) | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₂} B | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₂} B | |
| (@Semiring.toNonAssocSemiring.{v₂} B inst_3))) | |
| (@Algebra.toModule.{u, v₁} R A inst inst_1 inst_2) | |
| (@Algebra.toModule.{u, v₂} R B inst inst_3 inst_4)) | |
| (@TensorProduct.instModuleTensorProductToSemiringAddCommMonoid.{u, v₁, v₂} R inst A B | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₁} A | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₁} A | |
| (@Semiring.toNonAssocSemiring.{v₁} A inst_1))) | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₂} B | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₂} B | |
| (@Semiring.toNonAssocSemiring.{v₂} B inst_3))) | |
| (@Algebra.toModule.{u, v₁} R A inst inst_1 inst_2) | |
| (@Algebra.toModule.{u, v₂} R B inst inst_3 inst_4))) | |
| (@CommSemiring.toSemiring.{u} R inst) (@CommSemiring.toSemiring.{u} R inst) | |
| (@TensorProduct.addCommMonoid.{u, v₁, v₂} R inst A B | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₁} A | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₁} A | |
| (@Semiring.toNonAssocSemiring.{v₁} A inst_1))) | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₂} B | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₂} B | |
| (@Semiring.toNonAssocSemiring.{v₂} B inst_3))) | |
| (@Algebra.toModule.{u, v₁} R A inst inst_1 inst_2) | |
| (@Algebra.toModule.{u, v₂} R B inst inst_3 inst_4)) | |
| (@LinearMap.addCommMonoid.{u, u, max v₁ v₂, max v₁ v₂} R R | |
| (@TensorProduct.{u, v₁, v₂} R inst A B | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₁} A | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₁} A | |
| (@Semiring.toNonAssocSemiring.{v₁} A inst_1))) | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₂} B | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₂} B | |
| (@Semiring.toNonAssocSemiring.{v₂} B inst_3))) | |
| (@Algebra.toModule.{u, v₁} R A inst inst_1 inst_2) | |
| (@Algebra.toModule.{u, v₂} R B inst inst_3 inst_4)) | |
| (@TensorProduct.{u, v₁, v₂} R inst A B | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₁} A | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₁} A | |
| (@Semiring.toNonAssocSemiring.{v₁} A inst_1))) | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₂} B | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₂} B | |
| (@Semiring.toNonAssocSemiring.{v₂} B inst_3))) | |
| (@Algebra.toModule.{u, v₁} R A inst inst_1 inst_2) | |
| (@Algebra.toModule.{u, v₂} R B inst inst_3 inst_4)) | |
| (@CommSemiring.toSemiring.{u} R inst) (@CommSemiring.toSemiring.{u} R inst) | |
| (@TensorProduct.addCommMonoid.{u, v₁, v₂} R inst A B | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₁} A | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₁} A | |
| (@Semiring.toNonAssocSemiring.{v₁} A inst_1))) | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₂} B | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₂} B | |
| (@Semiring.toNonAssocSemiring.{v₂} B inst_3))) | |
| (@Algebra.toModule.{u, v₁} R A inst inst_1 inst_2) | |
| (@Algebra.toModule.{u, v₂} R B inst inst_3 inst_4)) | |
| (@TensorProduct.addCommMonoid.{u, v₁, v₂} R inst A B | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₁} A | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₁} A | |
| (@Semiring.toNonAssocSemiring.{v₁} A inst_1))) | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₂} B | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₂} B | |
| (@Semiring.toNonAssocSemiring.{v₂} B inst_3))) | |
| (@Algebra.toModule.{u, v₁} R A inst inst_1 inst_2) | |
| (@Algebra.toModule.{u, v₂} R B inst inst_3 inst_4)) | |
| (@TensorProduct.instModuleTensorProductToSemiringAddCommMonoid.{u, v₁, v₂} R inst A B | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₁} A | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₁} A | |
| (@Semiring.toNonAssocSemiring.{v₁} A inst_1))) | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₂} B | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₂} B | |
| (@Semiring.toNonAssocSemiring.{v₂} B inst_3))) | |
| (@Algebra.toModule.{u, v₁} R A inst inst_1 inst_2) | |
| (@Algebra.toModule.{u, v₂} R B inst inst_3 inst_4)) | |
| (@TensorProduct.instModuleTensorProductToSemiringAddCommMonoid.{u, v₁, v₂} R inst A B | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₁} A | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₁} A | |
| (@Semiring.toNonAssocSemiring.{v₁} A inst_1))) | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₂} B | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₂} B | |
| (@Semiring.toNonAssocSemiring.{v₂} B inst_3))) | |
| (@Algebra.toModule.{u, v₁} R A inst inst_1 inst_2) | |
| (@Algebra.toModule.{u, v₂} R B inst inst_3 inst_4)) | |
| (@RingHom.id.{u} R (@Semiring.toNonAssocSemiring.{u} R (@CommSemiring.toSemiring.{u} R inst)))) | |
| (@TensorProduct.instModuleTensorProductToSemiringAddCommMonoid.{u, v₁, v₂} R inst A B | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₁} A | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₁} A | |
| (@Semiring.toNonAssocSemiring.{v₁} A inst_1))) | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₂} B | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₂} B | |
| (@Semiring.toNonAssocSemiring.{v₂} B inst_3))) | |
| (@Algebra.toModule.{u, v₁} R A inst inst_1 inst_2) | |
| (@Algebra.toModule.{u, v₂} R B inst inst_3 inst_4)) | |
| (@LinearMap.module.{u, u, u, max v₁ v₂, max v₁ v₂} R R R | |
| (@TensorProduct.{u, v₁, v₂} R inst A B | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₁} A | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₁} A | |
| (@Semiring.toNonAssocSemiring.{v₁} A inst_1))) | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₂} B | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₂} B | |
| (@Semiring.toNonAssocSemiring.{v₂} B inst_3))) | |
| (@Algebra.toModule.{u, v₁} R A inst inst_1 inst_2) | |
| (@Algebra.toModule.{u, v₂} R B inst inst_3 inst_4)) | |
| (@TensorProduct.{u, v₁, v₂} R inst A B | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₁} A | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₁} A | |
| (@Semiring.toNonAssocSemiring.{v₁} A inst_1))) | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₂} B | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₂} B | |
| (@Semiring.toNonAssocSemiring.{v₂} B inst_3))) | |
| (@Algebra.toModule.{u, v₁} R A inst inst_1 inst_2) | |
| (@Algebra.toModule.{u, v₂} R B inst inst_3 inst_4)) | |
| (@CommSemiring.toSemiring.{u} R inst) (@CommSemiring.toSemiring.{u} R inst) | |
| (@TensorProduct.addCommMonoid.{u, v₁, v₂} R inst A B | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₁} A | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₁} A | |
| (@Semiring.toNonAssocSemiring.{v₁} A inst_1))) | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₂} B | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₂} B | |
| (@Semiring.toNonAssocSemiring.{v₂} B inst_3))) | |
| (@Algebra.toModule.{u, v₁} R A inst inst_1 inst_2) | |
| (@Algebra.toModule.{u, v₂} R B inst inst_3 inst_4)) | |
| (@TensorProduct.addCommMonoid.{u, v₁, v₂} R inst A B | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₁} A | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₁} A | |
| (@Semiring.toNonAssocSemiring.{v₁} A inst_1))) | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₂} B | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₂} B | |
| (@Semiring.toNonAssocSemiring.{v₂} B inst_3))) | |
| (@Algebra.toModule.{u, v₁} R A inst inst_1 inst_2) | |
| (@Algebra.toModule.{u, v₂} R B inst inst_3 inst_4)) | |
| (@TensorProduct.instModuleTensorProductToSemiringAddCommMonoid.{u, v₁, v₂} R inst A B | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₁} A | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₁} A | |
| (@Semiring.toNonAssocSemiring.{v₁} A inst_1))) | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₂} B | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₂} B | |
| (@Semiring.toNonAssocSemiring.{v₂} B inst_3))) | |
| (@Algebra.toModule.{u, v₁} R A inst inst_1 inst_2) | |
| (@Algebra.toModule.{u, v₂} R B inst inst_3 inst_4)) | |
| (@TensorProduct.instModuleTensorProductToSemiringAddCommMonoid.{u, v₁, v₂} R inst A B | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₁} A | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₁} A | |
| (@Semiring.toNonAssocSemiring.{v₁} A inst_1))) | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₂} B | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₂} B | |
| (@Semiring.toNonAssocSemiring.{v₂} B inst_3))) | |
| (@Algebra.toModule.{u, v₁} R A inst inst_1 inst_2) | |
| (@Algebra.toModule.{u, v₂} R B inst inst_3 inst_4)) | |
| (@RingHom.id.{u} R (@Semiring.toNonAssocSemiring.{u} R (@CommSemiring.toSemiring.{u} R inst))) | |
| (@CommSemiring.toSemiring.{u} R inst) | |
| (@TensorProduct.instModuleTensorProductToSemiringAddCommMonoid.{u, v₁, v₂} R inst A B | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₁} A | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₁} A | |
| (@Semiring.toNonAssocSemiring.{v₁} A inst_1))) | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₂} B | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₂} B | |
| (@Semiring.toNonAssocSemiring.{v₂} B inst_3))) | |
| (@Algebra.toModule.{u, v₁} R A inst inst_1 inst_2) | |
| (@Algebra.toModule.{u, v₂} R B inst inst_3 inst_4)) | |
| (@Algebra.TensorProduct.instSemiring.proof_1.{u, v₁, v₂} R inst A inst_1 inst_2 B inst_3 | |
| inst_4)) | |
| (@RingHom.id.{u} R (@Semiring.toNonAssocSemiring.{u} R (@CommSemiring.toSemiring.{u} R inst)))) | |
| (@Algebra.TensorProduct.mul.{u, v₁, v₂} R inst A inst_1 inst_2 B inst_3 inst_4) a) | |
| b) | |
| (@Algebra.TensorProduct.instSemiring.proof_8.{u, v₁, v₂} R inst A inst_1 inst_2 B inst_3 inst_4) | |
| (@Algebra.TensorProduct.instSemiring.proof_9.{u, v₁, v₂} R inst A inst_1 inst_2 B inst_3 inst_4) | |
| (@Algebra.TensorProduct.instSemiring.proof_10.{u, v₁, v₂} R inst A inst_1 inst_2 B inst_3 inst_4) | |
| (@Algebra.TensorProduct.instSemiring.proof_11.{u, v₁, v₂} R inst A inst_1 inst_2 B inst_3 inst_4)) | |
| (@Algebra.TensorProduct.mul_assoc.{u, v₁, v₂} R inst A inst_1 inst_2 B inst_3 inst_4))))) | |
| (@Algebra.TensorProduct.instSemiring.proof_12.{u, v₁, v₂} R inst A inst_1 inst_2 B inst_3 inst_4) | |
| (@Algebra.TensorProduct.instSemiring.proof_13.{u, v₁, v₂} R inst A inst_1 inst_2 B inst_3 inst_4) |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| def Algebra.TensorProduct.instSemiring.{u, v₁, v₂} : {R : Type u} → | |
| [inst : CommSemiring.{u} R] → | |
| {A : Type v₁} → | |
| [inst_1 : Semiring.{v₁} A] → | |
| [inst_2 : @Algebra.{u, v₁} R A inst inst_1] → | |
| {B : Type v₂} → | |
| [inst_3 : Semiring.{v₂} B] → | |
| [inst_4 : @Algebra.{u, v₂} R B inst inst_3] → | |
| Semiring.{max v₂ v₁} | |
| (@TensorProduct.{u, v₁, v₂} R inst A B | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₁} A | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₁} A | |
| (@Semiring.toNonAssocSemiring.{v₁} A inst_1))) | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₂} B | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₂} B | |
| (@Semiring.toNonAssocSemiring.{v₂} B inst_3))) | |
| (@Algebra.toModule.{u, v₁} R A inst inst_1 inst_2) | |
| (@Algebra.toModule.{u, v₂} R B inst inst_3 inst_4)) := | |
| fun {R : Type u} [inst : CommSemiring.{u} R] {A : Type v₁} [inst_1 : Semiring.{v₁} A] | |
| [inst_2 : @Algebra.{u, v₁} R A inst inst_1] {B : Type v₂} [inst_3 : Semiring.{v₂} B] | |
| [inst_4 : @Algebra.{u, v₂} R B inst inst_3] ↦ | |
| let src : | |
| AddMonoidWithOne.{max v₂ v₁} | |
| (@TensorProduct.{u, v₁, v₂} R inst A B | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₁} A | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₁} A (@Semiring.toNonAssocSemiring.{v₁} A inst_1))) | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₂} B | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₂} B (@Semiring.toNonAssocSemiring.{v₂} B inst_3))) | |
| (@Algebra.toModule.{u, v₁} R A inst inst_1 inst_2) (@Algebra.toModule.{u, v₂} R B inst inst_3 inst_4)) := | |
| @inferInstance.{max (v₁ + 1) (v₂ + 1)} | |
| (AddMonoidWithOne.{max v₂ v₁} | |
| (@TensorProduct.{u, v₁, v₂} R inst A B | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₁} A | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₁} A (@Semiring.toNonAssocSemiring.{v₁} A inst_1))) | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₂} B | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₂} B (@Semiring.toNonAssocSemiring.{v₂} B inst_3))) | |
| (@Algebra.toModule.{u, v₁} R A inst inst_1 inst_2) (@Algebra.toModule.{u, v₂} R B inst inst_3 inst_4))) | |
| (@Algebra.TensorProduct.instAddMonoidWithOneTensorProductToAddCommMonoidToNonUnitalNonAssocSemiringToNonAssocSemiringToAddCommMonoidToNonUnitalNonAssocSemiringToNonAssocSemiringToModuleToModule.{u, | |
| v₁, v₂} | |
| R inst A inst_1 inst_2 B inst_3 inst_4); | |
| let src_1 : | |
| AddCommMonoid.{max v₂ v₁} | |
| (@TensorProduct.{u, v₁, v₂} R inst A B | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₁} A | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₁} A (@Semiring.toNonAssocSemiring.{v₁} A inst_1))) | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₂} B | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₂} B (@Semiring.toNonAssocSemiring.{v₂} B inst_3))) | |
| (@Algebra.toModule.{u, v₁} R A inst inst_1 inst_2) (@Algebra.toModule.{u, v₂} R B inst inst_3 inst_4)) := | |
| @inferInstance.{max (v₁ + 1) (v₂ + 1)} | |
| (AddCommMonoid.{max v₂ v₁} | |
| (@TensorProduct.{u, v₁, v₂} R inst A B | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₁} A | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₁} A (@Semiring.toNonAssocSemiring.{v₁} A inst_1))) | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₂} B | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₂} B (@Semiring.toNonAssocSemiring.{v₂} B inst_3))) | |
| (@Algebra.toModule.{u, v₁} R A inst inst_1 inst_2) (@Algebra.toModule.{u, v₂} R B inst inst_3 inst_4))) | |
| (@Algebra.TensorProduct.instAddCommMonoidTensorProductToAddCommMonoidToNonUnitalNonAssocSemiringToNonAssocSemiringToAddCommMonoidToNonUnitalNonAssocSemiringToNonAssocSemiringToModuleToModule.{u, | |
| v₁, v₂} | |
| R inst A inst_1 inst_2 B inst_3 inst_4); | |
| @Semiring.mk.{max v₁ v₂} | |
| (@TensorProduct.{u, v₁, v₂} R inst A B | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₁} A | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₁} A (@Semiring.toNonAssocSemiring.{v₁} A inst_1))) | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₂} B | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₂} B (@Semiring.toNonAssocSemiring.{v₂} B inst_3))) | |
| (@Algebra.toModule.{u, v₁} R A inst inst_1 inst_2) (@Algebra.toModule.{u, v₂} R B inst inst_3 inst_4)) | |
| (@NonUnitalSemiring.mk.{max v₁ v₂} | |
| (@TensorProduct.{u, v₁, v₂} R inst A B | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₁} A | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₁} A (@Semiring.toNonAssocSemiring.{v₁} A inst_1))) | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₂} B | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₂} B (@Semiring.toNonAssocSemiring.{v₂} B inst_3))) | |
| (@Algebra.toModule.{u, v₁} R A inst inst_1 inst_2) (@Algebra.toModule.{u, v₂} R B inst inst_3 inst_4)) | |
| (@NonUnitalNonAssocSemiring.mk.{max v₁ v₂} | |
| (@TensorProduct.{u, v₁, v₂} R inst A B | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₁} A | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₁} A (@Semiring.toNonAssocSemiring.{v₁} A inst_1))) | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₂} B | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₂} B (@Semiring.toNonAssocSemiring.{v₂} B inst_3))) | |
| (@Algebra.toModule.{u, v₁} R A inst inst_1 inst_2) (@Algebra.toModule.{u, v₂} R B inst inst_3 inst_4)) | |
| (@AddCommMonoid.mk.{max v₁ v₂} | |
| (@TensorProduct.{u, v₁, v₂} R inst A B | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₁} A | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₁} A (@Semiring.toNonAssocSemiring.{v₁} A inst_1))) | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₂} B | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₂} B (@Semiring.toNonAssocSemiring.{v₂} B inst_3))) | |
| (@Algebra.toModule.{u, v₁} R A inst inst_1 inst_2) (@Algebra.toModule.{u, v₂} R B inst inst_3 inst_4)) | |
| (@AddMonoid.mk.{max v₁ v₂} | |
| (@TensorProduct.{u, v₁, v₂} R inst A B | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₁} A | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₁} A (@Semiring.toNonAssocSemiring.{v₁} A inst_1))) | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₂} B | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₂} B (@Semiring.toNonAssocSemiring.{v₂} B inst_3))) | |
| (@Algebra.toModule.{u, v₁} R A inst inst_1 inst_2) (@Algebra.toModule.{u, v₂} R B inst inst_3 inst_4)) | |
| (@AddSemigroup.mk.{max v₁ v₂} | |
| (@TensorProduct.{u, v₁, v₂} R inst A B | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₁} A | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₁} A (@Semiring.toNonAssocSemiring.{v₁} A inst_1))) | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₂} B | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₂} B (@Semiring.toNonAssocSemiring.{v₂} B inst_3))) | |
| (@Algebra.toModule.{u, v₁} R A inst inst_1 inst_2) (@Algebra.toModule.{u, v₂} R B inst inst_3 inst_4)) | |
| (@Add.mk.{max v₁ v₂} | |
| (@TensorProduct.{u, v₁, v₂} R inst A B | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₁} A | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₁} A (@Semiring.toNonAssocSemiring.{v₁} A inst_1))) | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₂} B | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₂} B (@Semiring.toNonAssocSemiring.{v₂} B inst_3))) | |
| (@Algebra.toModule.{u, v₁} R A inst inst_1 inst_2) (@Algebra.toModule.{u, v₂} R B inst inst_3 inst_4)) | |
| fun | |
| (x x_1 : | |
| @TensorProduct.{u, v₁, v₂} R inst A B | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₁} A | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₁} A | |
| (@Semiring.toNonAssocSemiring.{v₁} A inst_1))) | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₂} B | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₂} B | |
| (@Semiring.toNonAssocSemiring.{v₂} B inst_3))) | |
| (@Algebra.toModule.{u, v₁} R A inst inst_1 inst_2) | |
| (@Algebra.toModule.{u, v₂} R B inst inst_3 inst_4)) ↦ | |
| @HAdd.hAdd.{max v₁ v₂, max v₁ v₂, max v₁ v₂} | |
| (@TensorProduct.{u, v₁, v₂} R inst A B | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₁} A | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₁} A | |
| (@Semiring.toNonAssocSemiring.{v₁} A inst_1))) | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₂} B | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₂} B | |
| (@Semiring.toNonAssocSemiring.{v₂} B inst_3))) | |
| (@Algebra.toModule.{u, v₁} R A inst inst_1 inst_2) | |
| (@Algebra.toModule.{u, v₂} R B inst inst_3 inst_4)) | |
| (@TensorProduct.{u, v₁, v₂} R inst A B | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₁} A | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₁} A | |
| (@Semiring.toNonAssocSemiring.{v₁} A inst_1))) | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₂} B | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₂} B | |
| (@Semiring.toNonAssocSemiring.{v₂} B inst_3))) | |
| (@Algebra.toModule.{u, v₁} R A inst inst_1 inst_2) | |
| (@Algebra.toModule.{u, v₂} R B inst inst_3 inst_4)) | |
| (@TensorProduct.{u, v₁, v₂} R inst A B | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₁} A | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₁} A | |
| (@Semiring.toNonAssocSemiring.{v₁} A inst_1))) | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₂} B | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₂} B | |
| (@Semiring.toNonAssocSemiring.{v₂} B inst_3))) | |
| (@Algebra.toModule.{u, v₁} R A inst inst_1 inst_2) | |
| (@Algebra.toModule.{u, v₂} R B inst inst_3 inst_4)) | |
| (@instHAdd.{max v₁ v₂} | |
| (@TensorProduct.{u, v₁, v₂} R inst A B | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₁} A | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₁} A | |
| (@Semiring.toNonAssocSemiring.{v₁} A inst_1))) | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₂} B | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₂} B | |
| (@Semiring.toNonAssocSemiring.{v₂} B inst_3))) | |
| (@Algebra.toModule.{u, v₁} R A inst inst_1 inst_2) | |
| (@Algebra.toModule.{u, v₂} R B inst inst_3 inst_4)) | |
| (@AddSemigroup.toAdd.{max v₁ v₂} | |
| (@TensorProduct.{u, v₁, v₂} R inst A B | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₁} A | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₁} A | |
| (@Semiring.toNonAssocSemiring.{v₁} A inst_1))) | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₂} B | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₂} B | |
| (@Semiring.toNonAssocSemiring.{v₂} B inst_3))) | |
| (@Algebra.toModule.{u, v₁} R A inst inst_1 inst_2) | |
| (@Algebra.toModule.{u, v₂} R B inst inst_3 inst_4)) | |
| (@AddMonoid.toAddSemigroup.{max v₁ v₂} | |
| (@TensorProduct.{u, v₁, v₂} R inst A B | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₁} A | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₁} A | |
| (@Semiring.toNonAssocSemiring.{v₁} A inst_1))) | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₂} B | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₂} B | |
| (@Semiring.toNonAssocSemiring.{v₂} B inst_3))) | |
| (@Algebra.toModule.{u, v₁} R A inst inst_1 inst_2) | |
| (@Algebra.toModule.{u, v₂} R B inst inst_3 inst_4)) | |
| (@AddMonoidWithOne.toAddMonoid.{max v₁ v₂} | |
| (@TensorProduct.{u, v₁, v₂} R inst A B | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₁} A | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₁} A | |
| (@Semiring.toNonAssocSemiring.{v₁} A inst_1))) | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₂} B | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₂} B | |
| (@Semiring.toNonAssocSemiring.{v₂} B inst_3))) | |
| (@Algebra.toModule.{u, v₁} R A inst inst_1 inst_2) | |
| (@Algebra.toModule.{u, v₂} R B inst inst_3 inst_4)) | |
| src)))) | |
| x x_1) | |
| (@Algebra.TensorProduct.instSemiring.proof_1.{u, v₁, v₂} R inst A inst_1 inst_2 B inst_3 inst_4)) | |
| (@Zero.mk.{max v₁ v₂} | |
| (@TensorProduct.{u, v₁, v₂} R inst A B | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₁} A | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₁} A (@Semiring.toNonAssocSemiring.{v₁} A inst_1))) | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₂} B | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₂} B (@Semiring.toNonAssocSemiring.{v₂} B inst_3))) | |
| (@Algebra.toModule.{u, v₁} R A inst inst_1 inst_2) (@Algebra.toModule.{u, v₂} R B inst inst_3 inst_4)) | |
| (@OfNat.ofNat.{max v₁ v₂} | |
| (@TensorProduct.{u, v₁, v₂} R inst A B | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₁} A | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₁} A (@Semiring.toNonAssocSemiring.{v₁} A inst_1))) | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₂} B | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₂} B (@Semiring.toNonAssocSemiring.{v₂} B inst_3))) | |
| (@Algebra.toModule.{u, v₁} R A inst inst_1 inst_2) (@Algebra.toModule.{u, v₂} R B inst inst_3 inst_4)) | |
| 0 | |
| (@Zero.toOfNat0.{max v₁ v₂} | |
| (@TensorProduct.{u, v₁, v₂} R inst A B | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₁} A | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₁} A | |
| (@Semiring.toNonAssocSemiring.{v₁} A inst_1))) | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₂} B | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₂} B | |
| (@Semiring.toNonAssocSemiring.{v₂} B inst_3))) | |
| (@Algebra.toModule.{u, v₁} R A inst inst_1 inst_2) | |
| (@Algebra.toModule.{u, v₂} R B inst inst_3 inst_4)) | |
| (@AddMonoid.toZero.{max v₁ v₂} | |
| (@TensorProduct.{u, v₁, v₂} R inst A B | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₁} A | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₁} A | |
| (@Semiring.toNonAssocSemiring.{v₁} A inst_1))) | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₂} B | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₂} B | |
| (@Semiring.toNonAssocSemiring.{v₂} B inst_3))) | |
| (@Algebra.toModule.{u, v₁} R A inst inst_1 inst_2) | |
| (@Algebra.toModule.{u, v₂} R B inst inst_3 inst_4)) | |
| (@AddMonoidWithOne.toAddMonoid.{max v₁ v₂} | |
| (@TensorProduct.{u, v₁, v₂} R inst A B | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₁} A | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₁} A | |
| (@Semiring.toNonAssocSemiring.{v₁} A inst_1))) | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₂} B | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₂} B | |
| (@Semiring.toNonAssocSemiring.{v₂} B inst_3))) | |
| (@Algebra.toModule.{u, v₁} R A inst inst_1 inst_2) | |
| (@Algebra.toModule.{u, v₂} R B inst inst_3 inst_4)) | |
| src))))) | |
| (@Algebra.TensorProduct.instSemiring.proof_2.{u, v₁, v₂} R inst A inst_1 inst_2 B inst_3 inst_4) | |
| (@Algebra.TensorProduct.instSemiring.proof_3.{u, v₁, v₂} R inst A inst_1 inst_2 B inst_3 inst_4) | |
| (@AddMonoid.nsmul.{max v₁ v₂} | |
| (@TensorProduct.{u, v₁, v₂} R inst A B | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₁} A | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₁} A (@Semiring.toNonAssocSemiring.{v₁} A inst_1))) | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₂} B | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₂} B (@Semiring.toNonAssocSemiring.{v₂} B inst_3))) | |
| (@Algebra.toModule.{u, v₁} R A inst inst_1 inst_2) (@Algebra.toModule.{u, v₂} R B inst inst_3 inst_4)) | |
| (@AddMonoidWithOne.toAddMonoid.{max v₁ v₂} | |
| (@TensorProduct.{u, v₁, v₂} R inst A B | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₁} A | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₁} A (@Semiring.toNonAssocSemiring.{v₁} A inst_1))) | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₂} B | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₂} B (@Semiring.toNonAssocSemiring.{v₂} B inst_3))) | |
| (@Algebra.toModule.{u, v₁} R A inst inst_1 inst_2) (@Algebra.toModule.{u, v₂} R B inst inst_3 inst_4)) | |
| src)) | |
| (@Algebra.TensorProduct.instSemiring.proof_4.{u, v₁, v₂} R inst A inst_1 inst_2 B inst_3 inst_4) | |
| (@Algebra.TensorProduct.instSemiring.proof_5.{u, v₁, v₂} R inst A inst_1 inst_2 B inst_3 inst_4)) | |
| (@Algebra.TensorProduct.instSemiring.proof_6.{u, v₁, v₂} R inst A inst_1 inst_2 B inst_3 inst_4)) | |
| (@Mul.mk.{max v₁ v₂} | |
| (@TensorProduct.{u, v₁, v₂} R inst A B | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₁} A | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₁} A (@Semiring.toNonAssocSemiring.{v₁} A inst_1))) | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₂} B | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₂} B (@Semiring.toNonAssocSemiring.{v₂} B inst_3))) | |
| (@Algebra.toModule.{u, v₁} R A inst inst_1 inst_2) (@Algebra.toModule.{u, v₂} R B inst inst_3 inst_4)) | |
| fun | |
| (a b : | |
| @TensorProduct.{u, v₁, v₂} R inst A B | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₁} A | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₁} A (@Semiring.toNonAssocSemiring.{v₁} A inst_1))) | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₂} B | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₂} B (@Semiring.toNonAssocSemiring.{v₂} B inst_3))) | |
| (@Algebra.toModule.{u, v₁} R A inst inst_1 inst_2) (@Algebra.toModule.{u, v₂} R B inst inst_3 inst_4)) ↦ | |
| @FunLike.coe.{max (v₁ + 1) (v₂ + 1), max (v₁ + 1) (v₂ + 1), max (v₁ + 1) (v₂ + 1)} | |
| ((fun | |
| (x : | |
| @TensorProduct.{u, v₁, v₂} R inst A B | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₁} A | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₁} A | |
| (@Semiring.toNonAssocSemiring.{v₁} A inst_1))) | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₂} B | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₂} B | |
| (@Semiring.toNonAssocSemiring.{v₂} B inst_3))) | |
| (@Algebra.toModule.{u, v₁} R A inst inst_1 inst_2) | |
| (@Algebra.toModule.{u, v₂} R B inst inst_3 inst_4)) ↦ | |
| @LinearMap.{u, u, max v₂ v₁, max v₂ v₁} R R (@CommSemiring.toSemiring.{u} R inst) | |
| (@CommSemiring.toSemiring.{u} R inst) | |
| (@RingHom.id.{u} R (@Semiring.toNonAssocSemiring.{u} R (@CommSemiring.toSemiring.{u} R inst))) | |
| (@TensorProduct.{u, v₁, v₂} R inst A B | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₁} A | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₁} A | |
| (@Semiring.toNonAssocSemiring.{v₁} A inst_1))) | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₂} B | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₂} B | |
| (@Semiring.toNonAssocSemiring.{v₂} B inst_3))) | |
| (@Algebra.toModule.{u, v₁} R A inst inst_1 inst_2) | |
| (@Algebra.toModule.{u, v₂} R B inst inst_3 inst_4)) | |
| (@TensorProduct.{u, v₁, v₂} R inst A B | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₁} A | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₁} A | |
| (@Semiring.toNonAssocSemiring.{v₁} A inst_1))) | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₂} B | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₂} B | |
| (@Semiring.toNonAssocSemiring.{v₂} B inst_3))) | |
| (@Algebra.toModule.{u, v₁} R A inst inst_1 inst_2) | |
| (@Algebra.toModule.{u, v₂} R B inst inst_3 inst_4)) | |
| (@TensorProduct.addCommMonoid.{u, v₁, v₂} R inst A B | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₁} A | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₁} A | |
| (@Semiring.toNonAssocSemiring.{v₁} A inst_1))) | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₂} B | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₂} B | |
| (@Semiring.toNonAssocSemiring.{v₂} B inst_3))) | |
| (@Algebra.toModule.{u, v₁} R A inst inst_1 inst_2) | |
| (@Algebra.toModule.{u, v₂} R B inst inst_3 inst_4)) | |
| (@TensorProduct.addCommMonoid.{u, v₁, v₂} R inst A B | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₁} A | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₁} A | |
| (@Semiring.toNonAssocSemiring.{v₁} A inst_1))) | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₂} B | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₂} B | |
| (@Semiring.toNonAssocSemiring.{v₂} B inst_3))) | |
| (@Algebra.toModule.{u, v₁} R A inst inst_1 inst_2) | |
| (@Algebra.toModule.{u, v₂} R B inst inst_3 inst_4)) | |
| (@TensorProduct.instModuleTensorProductToSemiringAddCommMonoid.{u, v₁, v₂} R inst A B | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₁} A | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₁} A | |
| (@Semiring.toNonAssocSemiring.{v₁} A inst_1))) | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₂} B | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₂} B | |
| (@Semiring.toNonAssocSemiring.{v₂} B inst_3))) | |
| (@Algebra.toModule.{u, v₁} R A inst inst_1 inst_2) | |
| (@Algebra.toModule.{u, v₂} R B inst inst_3 inst_4)) | |
| (@TensorProduct.instModuleTensorProductToSemiringAddCommMonoid.{u, v₁, v₂} R inst A B | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₁} A | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₁} A | |
| (@Semiring.toNonAssocSemiring.{v₁} A inst_1))) | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₂} B | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₂} B | |
| (@Semiring.toNonAssocSemiring.{v₂} B inst_3))) | |
| (@Algebra.toModule.{u, v₁} R A inst inst_1 inst_2) | |
| (@Algebra.toModule.{u, v₂} R B inst inst_3 inst_4))) | |
| a) | |
| (@TensorProduct.{u, v₁, v₂} R inst A B | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₁} A | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₁} A (@Semiring.toNonAssocSemiring.{v₁} A inst_1))) | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₂} B | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₂} B (@Semiring.toNonAssocSemiring.{v₂} B inst_3))) | |
| (@Algebra.toModule.{u, v₁} R A inst inst_1 inst_2) (@Algebra.toModule.{u, v₂} R B inst inst_3 inst_4)) | |
| (fun | |
| (a : | |
| @TensorProduct.{u, v₁, v₂} R inst A B | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₁} A | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₁} A | |
| (@Semiring.toNonAssocSemiring.{v₁} A inst_1))) | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₂} B | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₂} B | |
| (@Semiring.toNonAssocSemiring.{v₂} B inst_3))) | |
| (@Algebra.toModule.{u, v₁} R A inst inst_1 inst_2) | |
| (@Algebra.toModule.{u, v₂} R B inst inst_3 inst_4)) ↦ | |
| (fun | |
| (x : | |
| @TensorProduct.{u, v₁, v₂} R inst A B | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₁} A | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₁} A | |
| (@Semiring.toNonAssocSemiring.{v₁} A inst_1))) | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₂} B | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₂} B | |
| (@Semiring.toNonAssocSemiring.{v₂} B inst_3))) | |
| (@Algebra.toModule.{u, v₁} R A inst inst_1 inst_2) | |
| (@Algebra.toModule.{u, v₂} R B inst inst_3 inst_4)) ↦ | |
| @TensorProduct.{u, v₁, v₂} R inst A B | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₁} A | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₁} A | |
| (@Semiring.toNonAssocSemiring.{v₁} A inst_1))) | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₂} B | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₂} B | |
| (@Semiring.toNonAssocSemiring.{v₂} B inst_3))) | |
| (@Algebra.toModule.{u, v₁} R A inst inst_1 inst_2) | |
| (@Algebra.toModule.{u, v₂} R B inst inst_3 inst_4)) | |
| a) | |
| (@LinearMap.instFunLikeLinearMap.{u, u, max v₁ v₂, max v₁ v₂} R R | |
| (@TensorProduct.{u, v₁, v₂} R inst A B | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₁} A | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₁} A (@Semiring.toNonAssocSemiring.{v₁} A inst_1))) | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₂} B | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₂} B (@Semiring.toNonAssocSemiring.{v₂} B inst_3))) | |
| (@Algebra.toModule.{u, v₁} R A inst inst_1 inst_2) (@Algebra.toModule.{u, v₂} R B inst inst_3 inst_4)) | |
| (@TensorProduct.{u, v₁, v₂} R inst A B | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₁} A | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₁} A (@Semiring.toNonAssocSemiring.{v₁} A inst_1))) | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₂} B | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₂} B (@Semiring.toNonAssocSemiring.{v₂} B inst_3))) | |
| (@Algebra.toModule.{u, v₁} R A inst inst_1 inst_2) (@Algebra.toModule.{u, v₂} R B inst inst_3 inst_4)) | |
| (@CommSemiring.toSemiring.{u} R inst) (@CommSemiring.toSemiring.{u} R inst) | |
| (@TensorProduct.addCommMonoid.{u, v₁, v₂} R inst A B | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₁} A | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₁} A (@Semiring.toNonAssocSemiring.{v₁} A inst_1))) | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₂} B | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₂} B (@Semiring.toNonAssocSemiring.{v₂} B inst_3))) | |
| (@Algebra.toModule.{u, v₁} R A inst inst_1 inst_2) (@Algebra.toModule.{u, v₂} R B inst inst_3 inst_4)) | |
| (@TensorProduct.addCommMonoid.{u, v₁, v₂} R inst A B | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₁} A | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₁} A (@Semiring.toNonAssocSemiring.{v₁} A inst_1))) | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₂} B | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₂} B (@Semiring.toNonAssocSemiring.{v₂} B inst_3))) | |
| (@Algebra.toModule.{u, v₁} R A inst inst_1 inst_2) (@Algebra.toModule.{u, v₂} R B inst inst_3 inst_4)) | |
| (@TensorProduct.instModuleTensorProductToSemiringAddCommMonoid.{u, v₁, v₂} R inst A B | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₁} A | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₁} A (@Semiring.toNonAssocSemiring.{v₁} A inst_1))) | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₂} B | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₂} B (@Semiring.toNonAssocSemiring.{v₂} B inst_3))) | |
| (@Algebra.toModule.{u, v₁} R A inst inst_1 inst_2) (@Algebra.toModule.{u, v₂} R B inst inst_3 inst_4)) | |
| (@TensorProduct.instModuleTensorProductToSemiringAddCommMonoid.{u, v₁, v₂} R inst A B | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₁} A | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₁} A (@Semiring.toNonAssocSemiring.{v₁} A inst_1))) | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₂} B | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₂} B (@Semiring.toNonAssocSemiring.{v₂} B inst_3))) | |
| (@Algebra.toModule.{u, v₁} R A inst inst_1 inst_2) (@Algebra.toModule.{u, v₂} R B inst inst_3 inst_4)) | |
| (@RingHom.id.{u} R (@Semiring.toNonAssocSemiring.{u} R (@CommSemiring.toSemiring.{u} R inst)))) | |
| (@FunLike.coe.{max (v₂ + 1) (v₁ + 1), max (v₂ + 1) (v₁ + 1), max (v₂ + 1) (v₁ + 1)} | |
| (@LinearMap.{u, u, max v₂ v₁, max v₂ v₁} R R (@CommSemiring.toSemiring.{u} R inst) | |
| (@CommSemiring.toSemiring.{u} R inst) | |
| (@RingHom.id.{u} R (@Semiring.toNonAssocSemiring.{u} R (@CommSemiring.toSemiring.{u} R inst))) | |
| (@TensorProduct.{u, v₁, v₂} R inst A B | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₁} A | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₁} A (@Semiring.toNonAssocSemiring.{v₁} A inst_1))) | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₂} B | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₂} B (@Semiring.toNonAssocSemiring.{v₂} B inst_3))) | |
| (@Algebra.toModule.{u, v₁} R A inst inst_1 inst_2) (@Algebra.toModule.{u, v₂} R B inst inst_3 inst_4)) | |
| (@LinearMap.{u, u, max v₂ v₁, max v₂ v₁} R R (@CommSemiring.toSemiring.{u} R inst) | |
| (@CommSemiring.toSemiring.{u} R inst) | |
| (@RingHom.id.{u} R (@Semiring.toNonAssocSemiring.{u} R (@CommSemiring.toSemiring.{u} R inst))) | |
| (@TensorProduct.{u, v₁, v₂} R inst A B | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₁} A | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₁} A | |
| (@Semiring.toNonAssocSemiring.{v₁} A inst_1))) | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₂} B | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₂} B | |
| (@Semiring.toNonAssocSemiring.{v₂} B inst_3))) | |
| (@Algebra.toModule.{u, v₁} R A inst inst_1 inst_2) | |
| (@Algebra.toModule.{u, v₂} R B inst inst_3 inst_4)) | |
| (@TensorProduct.{u, v₁, v₂} R inst A B | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₁} A | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₁} A | |
| (@Semiring.toNonAssocSemiring.{v₁} A inst_1))) | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₂} B | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₂} B | |
| (@Semiring.toNonAssocSemiring.{v₂} B inst_3))) | |
| (@Algebra.toModule.{u, v₁} R A inst inst_1 inst_2) | |
| (@Algebra.toModule.{u, v₂} R B inst inst_3 inst_4)) | |
| (@TensorProduct.addCommMonoid.{u, v₁, v₂} R inst A B | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₁} A | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₁} A | |
| (@Semiring.toNonAssocSemiring.{v₁} A inst_1))) | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₂} B | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₂} B | |
| (@Semiring.toNonAssocSemiring.{v₂} B inst_3))) | |
| (@Algebra.toModule.{u, v₁} R A inst inst_1 inst_2) | |
| (@Algebra.toModule.{u, v₂} R B inst inst_3 inst_4)) | |
| (@TensorProduct.addCommMonoid.{u, v₁, v₂} R inst A B | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₁} A | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₁} A | |
| (@Semiring.toNonAssocSemiring.{v₁} A inst_1))) | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₂} B | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₂} B | |
| (@Semiring.toNonAssocSemiring.{v₂} B inst_3))) | |
| (@Algebra.toModule.{u, v₁} R A inst inst_1 inst_2) | |
| (@Algebra.toModule.{u, v₂} R B inst inst_3 inst_4)) | |
| (@TensorProduct.instModuleTensorProductToSemiringAddCommMonoid.{u, v₁, v₂} R inst A B | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₁} A | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₁} A | |
| (@Semiring.toNonAssocSemiring.{v₁} A inst_1))) | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₂} B | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₂} B | |
| (@Semiring.toNonAssocSemiring.{v₂} B inst_3))) | |
| (@Algebra.toModule.{u, v₁} R A inst inst_1 inst_2) | |
| (@Algebra.toModule.{u, v₂} R B inst inst_3 inst_4)) | |
| (@TensorProduct.instModuleTensorProductToSemiringAddCommMonoid.{u, v₁, v₂} R inst A B | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₁} A | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₁} A | |
| (@Semiring.toNonAssocSemiring.{v₁} A inst_1))) | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₂} B | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₂} B | |
| (@Semiring.toNonAssocSemiring.{v₂} B inst_3))) | |
| (@Algebra.toModule.{u, v₁} R A inst inst_1 inst_2) | |
| (@Algebra.toModule.{u, v₂} R B inst inst_3 inst_4))) | |
| (@TensorProduct.addCommMonoid.{u, v₁, v₂} R inst A B | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₁} A | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₁} A (@Semiring.toNonAssocSemiring.{v₁} A inst_1))) | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₂} B | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₂} B (@Semiring.toNonAssocSemiring.{v₂} B inst_3))) | |
| (@Algebra.toModule.{u, v₁} R A inst inst_1 inst_2) (@Algebra.toModule.{u, v₂} R B inst inst_3 inst_4)) | |
| (@LinearMap.addCommMonoid.{u, u, max v₁ v₂, max v₁ v₂} R R | |
| (@TensorProduct.{u, v₁, v₂} R inst A B | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₁} A | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₁} A | |
| (@Semiring.toNonAssocSemiring.{v₁} A inst_1))) | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₂} B | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₂} B | |
| (@Semiring.toNonAssocSemiring.{v₂} B inst_3))) | |
| (@Algebra.toModule.{u, v₁} R A inst inst_1 inst_2) | |
| (@Algebra.toModule.{u, v₂} R B inst inst_3 inst_4)) | |
| (@TensorProduct.{u, v₁, v₂} R inst A B | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₁} A | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₁} A | |
| (@Semiring.toNonAssocSemiring.{v₁} A inst_1))) | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₂} B | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₂} B | |
| (@Semiring.toNonAssocSemiring.{v₂} B inst_3))) | |
| (@Algebra.toModule.{u, v₁} R A inst inst_1 inst_2) | |
| (@Algebra.toModule.{u, v₂} R B inst inst_3 inst_4)) | |
| (@CommSemiring.toSemiring.{u} R inst) (@CommSemiring.toSemiring.{u} R inst) | |
| (@TensorProduct.addCommMonoid.{u, v₁, v₂} R inst A B | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₁} A | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₁} A | |
| (@Semiring.toNonAssocSemiring.{v₁} A inst_1))) | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₂} B | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₂} B | |
| (@Semiring.toNonAssocSemiring.{v₂} B inst_3))) | |
| (@Algebra.toModule.{u, v₁} R A inst inst_1 inst_2) | |
| (@Algebra.toModule.{u, v₂} R B inst inst_3 inst_4)) | |
| (@TensorProduct.addCommMonoid.{u, v₁, v₂} R inst A B | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₁} A | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₁} A | |
| (@Semiring.toNonAssocSemiring.{v₁} A inst_1))) | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₂} B | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₂} B | |
| (@Semiring.toNonAssocSemiring.{v₂} B inst_3))) | |
| (@Algebra.toModule.{u, v₁} R A inst inst_1 inst_2) | |
| (@Algebra.toModule.{u, v₂} R B inst inst_3 inst_4)) | |
| (@TensorProduct.instModuleTensorProductToSemiringAddCommMonoid.{u, v₁, v₂} R inst A B | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₁} A | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₁} A | |
| (@Semiring.toNonAssocSemiring.{v₁} A inst_1))) | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₂} B | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₂} B | |
| (@Semiring.toNonAssocSemiring.{v₂} B inst_3))) | |
| (@Algebra.toModule.{u, v₁} R A inst inst_1 inst_2) | |
| (@Algebra.toModule.{u, v₂} R B inst inst_3 inst_4)) | |
| (@TensorProduct.instModuleTensorProductToSemiringAddCommMonoid.{u, v₁, v₂} R inst A B | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₁} A | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₁} A | |
| (@Semiring.toNonAssocSemiring.{v₁} A inst_1))) | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₂} B | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₂} B | |
| (@Semiring.toNonAssocSemiring.{v₂} B inst_3))) | |
| (@Algebra.toModule.{u, v₁} R A inst inst_1 inst_2) | |
| (@Algebra.toModule.{u, v₂} R B inst inst_3 inst_4)) | |
| (@RingHom.id.{u} R (@Semiring.toNonAssocSemiring.{u} R (@CommSemiring.toSemiring.{u} R inst)))) | |
| (@TensorProduct.instModuleTensorProductToSemiringAddCommMonoid.{u, v₁, v₂} R inst A B | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₁} A | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₁} A (@Semiring.toNonAssocSemiring.{v₁} A inst_1))) | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₂} B | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₂} B (@Semiring.toNonAssocSemiring.{v₂} B inst_3))) | |
| (@Algebra.toModule.{u, v₁} R A inst inst_1 inst_2) (@Algebra.toModule.{u, v₂} R B inst inst_3 inst_4)) | |
| (@LinearMap.module.{u, u, u, max v₁ v₂, max v₁ v₂} R R R | |
| (@TensorProduct.{u, v₁, v₂} R inst A B | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₁} A | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₁} A | |
| (@Semiring.toNonAssocSemiring.{v₁} A inst_1))) | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₂} B | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₂} B | |
| (@Semiring.toNonAssocSemiring.{v₂} B inst_3))) | |
| (@Algebra.toModule.{u, v₁} R A inst inst_1 inst_2) | |
| (@Algebra.toModule.{u, v₂} R B inst inst_3 inst_4)) | |
| (@TensorProduct.{u, v₁, v₂} R inst A B | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₁} A | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₁} A | |
| (@Semiring.toNonAssocSemiring.{v₁} A inst_1))) | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₂} B | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₂} B | |
| (@Semiring.toNonAssocSemiring.{v₂} B inst_3))) | |
| (@Algebra.toModule.{u, v₁} R A inst inst_1 inst_2) | |
| (@Algebra.toModule.{u, v₂} R B inst inst_3 inst_4)) | |
| (@CommSemiring.toSemiring.{u} R inst) (@CommSemiring.toSemiring.{u} R inst) | |
| (@TensorProduct.addCommMonoid.{u, v₁, v₂} R inst A B | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₁} A | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₁} A | |
| (@Semiring.toNonAssocSemiring.{v₁} A inst_1))) | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₂} B | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₂} B | |
| (@Semiring.toNonAssocSemiring.{v₂} B inst_3))) | |
| (@Algebra.toModule.{u, v₁} R A inst inst_1 inst_2) | |
| (@Algebra.toModule.{u, v₂} R B inst inst_3 inst_4)) | |
| (@TensorProduct.addCommMonoid.{u, v₁, v₂} R inst A B | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₁} A | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₁} A | |
| (@Semiring.toNonAssocSemiring.{v₁} A inst_1))) | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₂} B | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₂} B | |
| (@Semiring.toNonAssocSemiring.{v₂} B inst_3))) | |
| (@Algebra.toModule.{u, v₁} R A inst inst_1 inst_2) | |
| (@Algebra.toModule.{u, v₂} R B inst inst_3 inst_4)) | |
| (@TensorProduct.instModuleTensorProductToSemiringAddCommMonoid.{u, v₁, v₂} R inst A B | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₁} A | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₁} A | |
| (@Semiring.toNonAssocSemiring.{v₁} A inst_1))) | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₂} B | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₂} B | |
| (@Semiring.toNonAssocSemiring.{v₂} B inst_3))) | |
| (@Algebra.toModule.{u, v₁} R A inst inst_1 inst_2) | |
| (@Algebra.toModule.{u, v₂} R B inst inst_3 inst_4)) | |
| (@TensorProduct.instModuleTensorProductToSemiringAddCommMonoid.{u, v₁, v₂} R inst A B | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₁} A | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₁} A | |
| (@Semiring.toNonAssocSemiring.{v₁} A inst_1))) | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₂} B | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₂} B | |
| (@Semiring.toNonAssocSemiring.{v₂} B inst_3))) | |
| (@Algebra.toModule.{u, v₁} R A inst inst_1 inst_2) | |
| (@Algebra.toModule.{u, v₂} R B inst inst_3 inst_4)) | |
| (@RingHom.id.{u} R (@Semiring.toNonAssocSemiring.{u} R (@CommSemiring.toSemiring.{u} R inst))) | |
| (@CommSemiring.toSemiring.{u} R inst) | |
| (@TensorProduct.instModuleTensorProductToSemiringAddCommMonoid.{u, v₁, v₂} R inst A B | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₁} A | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₁} A | |
| (@Semiring.toNonAssocSemiring.{v₁} A inst_1))) | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₂} B | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₂} B | |
| (@Semiring.toNonAssocSemiring.{v₂} B inst_3))) | |
| (@Algebra.toModule.{u, v₁} R A inst inst_1 inst_2) | |
| (@Algebra.toModule.{u, v₂} R B inst inst_3 inst_4)) | |
| (@Algebra.TensorProduct.instSemiring.proof_7.{u, v₁, v₂} R inst A inst_1 inst_2 B inst_3 inst_4))) | |
| (@TensorProduct.{u, v₁, v₂} R inst A B | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₁} A | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₁} A (@Semiring.toNonAssocSemiring.{v₁} A inst_1))) | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₂} B | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₂} B (@Semiring.toNonAssocSemiring.{v₂} B inst_3))) | |
| (@Algebra.toModule.{u, v₁} R A inst inst_1 inst_2) (@Algebra.toModule.{u, v₂} R B inst inst_3 inst_4)) | |
| (fun | |
| (a : | |
| @TensorProduct.{u, v₁, v₂} R inst A B | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₁} A | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₁} A | |
| (@Semiring.toNonAssocSemiring.{v₁} A inst_1))) | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₂} B | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₂} B | |
| (@Semiring.toNonAssocSemiring.{v₂} B inst_3))) | |
| (@Algebra.toModule.{u, v₁} R A inst inst_1 inst_2) | |
| (@Algebra.toModule.{u, v₂} R B inst inst_3 inst_4)) ↦ | |
| (fun | |
| (x : | |
| @TensorProduct.{u, v₁, v₂} R inst A B | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₁} A | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₁} A | |
| (@Semiring.toNonAssocSemiring.{v₁} A inst_1))) | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₂} B | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₂} B | |
| (@Semiring.toNonAssocSemiring.{v₂} B inst_3))) | |
| (@Algebra.toModule.{u, v₁} R A inst inst_1 inst_2) | |
| (@Algebra.toModule.{u, v₂} R B inst inst_3 inst_4)) ↦ | |
| @LinearMap.{u, u, max v₂ v₁, max v₂ v₁} R R (@CommSemiring.toSemiring.{u} R inst) | |
| (@CommSemiring.toSemiring.{u} R inst) | |
| (@RingHom.id.{u} R (@Semiring.toNonAssocSemiring.{u} R (@CommSemiring.toSemiring.{u} R inst))) | |
| (@TensorProduct.{u, v₁, v₂} R inst A B | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₁} A | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₁} A | |
| (@Semiring.toNonAssocSemiring.{v₁} A inst_1))) | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₂} B | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₂} B | |
| (@Semiring.toNonAssocSemiring.{v₂} B inst_3))) | |
| (@Algebra.toModule.{u, v₁} R A inst inst_1 inst_2) | |
| (@Algebra.toModule.{u, v₂} R B inst inst_3 inst_4)) | |
| (@TensorProduct.{u, v₁, v₂} R inst A B | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₁} A | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₁} A | |
| (@Semiring.toNonAssocSemiring.{v₁} A inst_1))) | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₂} B | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₂} B | |
| (@Semiring.toNonAssocSemiring.{v₂} B inst_3))) | |
| (@Algebra.toModule.{u, v₁} R A inst inst_1 inst_2) | |
| (@Algebra.toModule.{u, v₂} R B inst inst_3 inst_4)) | |
| (@TensorProduct.addCommMonoid.{u, v₁, v₂} R inst A B | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₁} A | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₁} A | |
| (@Semiring.toNonAssocSemiring.{v₁} A inst_1))) | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₂} B | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₂} B | |
| (@Semiring.toNonAssocSemiring.{v₂} B inst_3))) | |
| (@Algebra.toModule.{u, v₁} R A inst inst_1 inst_2) | |
| (@Algebra.toModule.{u, v₂} R B inst inst_3 inst_4)) | |
| (@TensorProduct.addCommMonoid.{u, v₁, v₂} R inst A B | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₁} A | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₁} A | |
| (@Semiring.toNonAssocSemiring.{v₁} A inst_1))) | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₂} B | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₂} B | |
| (@Semiring.toNonAssocSemiring.{v₂} B inst_3))) | |
| (@Algebra.toModule.{u, v₁} R A inst inst_1 inst_2) | |
| (@Algebra.toModule.{u, v₂} R B inst inst_3 inst_4)) | |
| (@TensorProduct.instModuleTensorProductToSemiringAddCommMonoid.{u, v₁, v₂} R inst A B | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₁} A | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₁} A | |
| (@Semiring.toNonAssocSemiring.{v₁} A inst_1))) | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₂} B | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₂} B | |
| (@Semiring.toNonAssocSemiring.{v₂} B inst_3))) | |
| (@Algebra.toModule.{u, v₁} R A inst inst_1 inst_2) | |
| (@Algebra.toModule.{u, v₂} R B inst inst_3 inst_4)) | |
| (@TensorProduct.instModuleTensorProductToSemiringAddCommMonoid.{u, v₁, v₂} R inst A B | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₁} A | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₁} A | |
| (@Semiring.toNonAssocSemiring.{v₁} A inst_1))) | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₂} B | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₂} B | |
| (@Semiring.toNonAssocSemiring.{v₂} B inst_3))) | |
| (@Algebra.toModule.{u, v₁} R A inst inst_1 inst_2) | |
| (@Algebra.toModule.{u, v₂} R B inst inst_3 inst_4))) | |
| a) | |
| (@LinearMap.instFunLikeLinearMap.{u, u, max v₂ v₁, max v₂ v₁} R R | |
| (@TensorProduct.{u, v₁, v₂} R inst A B | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₁} A | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₁} A (@Semiring.toNonAssocSemiring.{v₁} A inst_1))) | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₂} B | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₂} B (@Semiring.toNonAssocSemiring.{v₂} B inst_3))) | |
| (@Algebra.toModule.{u, v₁} R A inst inst_1 inst_2) (@Algebra.toModule.{u, v₂} R B inst inst_3 inst_4)) | |
| (@LinearMap.{u, u, max v₂ v₁, max v₂ v₁} R R (@CommSemiring.toSemiring.{u} R inst) | |
| (@CommSemiring.toSemiring.{u} R inst) | |
| (@RingHom.id.{u} R (@Semiring.toNonAssocSemiring.{u} R (@CommSemiring.toSemiring.{u} R inst))) | |
| (@TensorProduct.{u, v₁, v₂} R inst A B | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₁} A | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₁} A | |
| (@Semiring.toNonAssocSemiring.{v₁} A inst_1))) | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₂} B | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₂} B | |
| (@Semiring.toNonAssocSemiring.{v₂} B inst_3))) | |
| (@Algebra.toModule.{u, v₁} R A inst inst_1 inst_2) | |
| (@Algebra.toModule.{u, v₂} R B inst inst_3 inst_4)) | |
| (@TensorProduct.{u, v₁, v₂} R inst A B | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₁} A | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₁} A | |
| (@Semiring.toNonAssocSemiring.{v₁} A inst_1))) | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₂} B | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₂} B | |
| (@Semiring.toNonAssocSemiring.{v₂} B inst_3))) | |
| (@Algebra.toModule.{u, v₁} R A inst inst_1 inst_2) | |
| (@Algebra.toModule.{u, v₂} R B inst inst_3 inst_4)) | |
| (@TensorProduct.addCommMonoid.{u, v₁, v₂} R inst A B | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₁} A | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₁} A | |
| (@Semiring.toNonAssocSemiring.{v₁} A inst_1))) | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₂} B | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₂} B | |
| (@Semiring.toNonAssocSemiring.{v₂} B inst_3))) | |
| (@Algebra.toModule.{u, v₁} R A inst inst_1 inst_2) | |
| (@Algebra.toModule.{u, v₂} R B inst inst_3 inst_4)) | |
| (@TensorProduct.addCommMonoid.{u, v₁, v₂} R inst A B | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₁} A | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₁} A | |
| (@Semiring.toNonAssocSemiring.{v₁} A inst_1))) | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₂} B | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₂} B | |
| (@Semiring.toNonAssocSemiring.{v₂} B inst_3))) | |
| (@Algebra.toModule.{u, v₁} R A inst inst_1 inst_2) | |
| (@Algebra.toModule.{u, v₂} R B inst inst_3 inst_4)) | |
| (@TensorProduct.instModuleTensorProductToSemiringAddCommMonoid.{u, v₁, v₂} R inst A B | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₁} A | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₁} A | |
| (@Semiring.toNonAssocSemiring.{v₁} A inst_1))) | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₂} B | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₂} B | |
| (@Semiring.toNonAssocSemiring.{v₂} B inst_3))) | |
| (@Algebra.toModule.{u, v₁} R A inst inst_1 inst_2) | |
| (@Algebra.toModule.{u, v₂} R B inst inst_3 inst_4)) | |
| (@TensorProduct.instModuleTensorProductToSemiringAddCommMonoid.{u, v₁, v₂} R inst A B | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₁} A | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₁} A | |
| (@Semiring.toNonAssocSemiring.{v₁} A inst_1))) | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₂} B | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₂} B | |
| (@Semiring.toNonAssocSemiring.{v₂} B inst_3))) | |
| (@Algebra.toModule.{u, v₁} R A inst inst_1 inst_2) | |
| (@Algebra.toModule.{u, v₂} R B inst inst_3 inst_4))) | |
| (@CommSemiring.toSemiring.{u} R inst) (@CommSemiring.toSemiring.{u} R inst) | |
| (@TensorProduct.addCommMonoid.{u, v₁, v₂} R inst A B | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₁} A | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₁} A (@Semiring.toNonAssocSemiring.{v₁} A inst_1))) | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₂} B | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₂} B (@Semiring.toNonAssocSemiring.{v₂} B inst_3))) | |
| (@Algebra.toModule.{u, v₁} R A inst inst_1 inst_2) (@Algebra.toModule.{u, v₂} R B inst inst_3 inst_4)) | |
| (@LinearMap.addCommMonoid.{u, u, max v₁ v₂, max v₁ v₂} R R | |
| (@TensorProduct.{u, v₁, v₂} R inst A B | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₁} A | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₁} A | |
| (@Semiring.toNonAssocSemiring.{v₁} A inst_1))) | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₂} B | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₂} B | |
| (@Semiring.toNonAssocSemiring.{v₂} B inst_3))) | |
| (@Algebra.toModule.{u, v₁} R A inst inst_1 inst_2) | |
| (@Algebra.toModule.{u, v₂} R B inst inst_3 inst_4)) | |
| (@TensorProduct.{u, v₁, v₂} R inst A B | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₁} A | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₁} A | |
| (@Semiring.toNonAssocSemiring.{v₁} A inst_1))) | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₂} B | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₂} B | |
| (@Semiring.toNonAssocSemiring.{v₂} B inst_3))) | |
| (@Algebra.toModule.{u, v₁} R A inst inst_1 inst_2) | |
| (@Algebra.toModule.{u, v₂} R B inst inst_3 inst_4)) | |
| (@CommSemiring.toSemiring.{u} R inst) (@CommSemiring.toSemiring.{u} R inst) | |
| (@TensorProduct.addCommMonoid.{u, v₁, v₂} R inst A B | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₁} A | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₁} A | |
| (@Semiring.toNonAssocSemiring.{v₁} A inst_1))) | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₂} B | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₂} B | |
| (@Semiring.toNonAssocSemiring.{v₂} B inst_3))) | |
| (@Algebra.toModule.{u, v₁} R A inst inst_1 inst_2) | |
| (@Algebra.toModule.{u, v₂} R B inst inst_3 inst_4)) | |
| (@TensorProduct.addCommMonoid.{u, v₁, v₂} R inst A B | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₁} A | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₁} A | |
| (@Semiring.toNonAssocSemiring.{v₁} A inst_1))) | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₂} B | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₂} B | |
| (@Semiring.toNonAssocSemiring.{v₂} B inst_3))) | |
| (@Algebra.toModule.{u, v₁} R A inst inst_1 inst_2) | |
| (@Algebra.toModule.{u, v₂} R B inst inst_3 inst_4)) | |
| (@TensorProduct.instModuleTensorProductToSemiringAddCommMonoid.{u, v₁, v₂} R inst A B | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₁} A | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₁} A | |
| (@Semiring.toNonAssocSemiring.{v₁} A inst_1))) | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₂} B | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₂} B | |
| (@Semiring.toNonAssocSemiring.{v₂} B inst_3))) | |
| (@Algebra.toModule.{u, v₁} R A inst inst_1 inst_2) | |
| (@Algebra.toModule.{u, v₂} R B inst inst_3 inst_4)) | |
| (@TensorProduct.instModuleTensorProductToSemiringAddCommMonoid.{u, v₁, v₂} R inst A B | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₁} A | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₁} A | |
| (@Semiring.toNonAssocSemiring.{v₁} A inst_1))) | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₂} B | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₂} B | |
| (@Semiring.toNonAssocSemiring.{v₂} B inst_3))) | |
| (@Algebra.toModule.{u, v₁} R A inst inst_1 inst_2) | |
| (@Algebra.toModule.{u, v₂} R B inst inst_3 inst_4)) | |
| (@RingHom.id.{u} R (@Semiring.toNonAssocSemiring.{u} R (@CommSemiring.toSemiring.{u} R inst)))) | |
| (@TensorProduct.instModuleTensorProductToSemiringAddCommMonoid.{u, v₁, v₂} R inst A B | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₁} A | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₁} A (@Semiring.toNonAssocSemiring.{v₁} A inst_1))) | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₂} B | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₂} B (@Semiring.toNonAssocSemiring.{v₂} B inst_3))) | |
| (@Algebra.toModule.{u, v₁} R A inst inst_1 inst_2) (@Algebra.toModule.{u, v₂} R B inst inst_3 inst_4)) | |
| (@LinearMap.module.{u, u, u, max v₁ v₂, max v₁ v₂} R R R | |
| (@TensorProduct.{u, v₁, v₂} R inst A B | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₁} A | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₁} A | |
| (@Semiring.toNonAssocSemiring.{v₁} A inst_1))) | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₂} B | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₂} B | |
| (@Semiring.toNonAssocSemiring.{v₂} B inst_3))) | |
| (@Algebra.toModule.{u, v₁} R A inst inst_1 inst_2) | |
| (@Algebra.toModule.{u, v₂} R B inst inst_3 inst_4)) | |
| (@TensorProduct.{u, v₁, v₂} R inst A B | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₁} A | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₁} A | |
| (@Semiring.toNonAssocSemiring.{v₁} A inst_1))) | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₂} B | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₂} B | |
| (@Semiring.toNonAssocSemiring.{v₂} B inst_3))) | |
| (@Algebra.toModule.{u, v₁} R A inst inst_1 inst_2) | |
| (@Algebra.toModule.{u, v₂} R B inst inst_3 inst_4)) | |
| (@CommSemiring.toSemiring.{u} R inst) (@CommSemiring.toSemiring.{u} R inst) | |
| (@TensorProduct.addCommMonoid.{u, v₁, v₂} R inst A B | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₁} A | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₁} A | |
| (@Semiring.toNonAssocSemiring.{v₁} A inst_1))) | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₂} B | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₂} B | |
| (@Semiring.toNonAssocSemiring.{v₂} B inst_3))) | |
| (@Algebra.toModule.{u, v₁} R A inst inst_1 inst_2) | |
| (@Algebra.toModule.{u, v₂} R B inst inst_3 inst_4)) | |
| (@TensorProduct.addCommMonoid.{u, v₁, v₂} R inst A B | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₁} A | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₁} A | |
| (@Semiring.toNonAssocSemiring.{v₁} A inst_1))) | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₂} B | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₂} B | |
| (@Semiring.toNonAssocSemiring.{v₂} B inst_3))) | |
| (@Algebra.toModule.{u, v₁} R A inst inst_1 inst_2) | |
| (@Algebra.toModule.{u, v₂} R B inst inst_3 inst_4)) | |
| (@TensorProduct.instModuleTensorProductToSemiringAddCommMonoid.{u, v₁, v₂} R inst A B | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₁} A | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₁} A | |
| (@Semiring.toNonAssocSemiring.{v₁} A inst_1))) | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₂} B | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₂} B | |
| (@Semiring.toNonAssocSemiring.{v₂} B inst_3))) | |
| (@Algebra.toModule.{u, v₁} R A inst inst_1 inst_2) | |
| (@Algebra.toModule.{u, v₂} R B inst inst_3 inst_4)) | |
| (@TensorProduct.instModuleTensorProductToSemiringAddCommMonoid.{u, v₁, v₂} R inst A B | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₁} A | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₁} A | |
| (@Semiring.toNonAssocSemiring.{v₁} A inst_1))) | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₂} B | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₂} B | |
| (@Semiring.toNonAssocSemiring.{v₂} B inst_3))) | |
| (@Algebra.toModule.{u, v₁} R A inst inst_1 inst_2) | |
| (@Algebra.toModule.{u, v₂} R B inst inst_3 inst_4)) | |
| (@RingHom.id.{u} R (@Semiring.toNonAssocSemiring.{u} R (@CommSemiring.toSemiring.{u} R inst))) | |
| (@CommSemiring.toSemiring.{u} R inst) | |
| (@TensorProduct.instModuleTensorProductToSemiringAddCommMonoid.{u, v₁, v₂} R inst A B | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₁} A | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₁} A | |
| (@Semiring.toNonAssocSemiring.{v₁} A inst_1))) | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₂} B | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₂} B | |
| (@Semiring.toNonAssocSemiring.{v₂} B inst_3))) | |
| (@Algebra.toModule.{u, v₁} R A inst inst_1 inst_2) | |
| (@Algebra.toModule.{u, v₂} R B inst inst_3 inst_4)) | |
| (@Algebra.TensorProduct.instSemiring.proof_7.{u, v₁, v₂} R inst A inst_1 inst_2 B inst_3 inst_4)) | |
| (@RingHom.id.{u} R (@Semiring.toNonAssocSemiring.{u} R (@CommSemiring.toSemiring.{u} R inst)))) | |
| (@Algebra.TensorProduct.mul.{u, v₁, v₂} R inst A inst_1 inst_2 B inst_3 inst_4) a) | |
| b) | |
| (@Algebra.TensorProduct.instSemiring.proof_8.{u, v₁, v₂} R inst A inst_1 inst_2 B inst_3 inst_4) | |
| (@Algebra.TensorProduct.instSemiring.proof_9.{u, v₁, v₂} R inst A inst_1 inst_2 B inst_3 inst_4) | |
| (@Algebra.TensorProduct.instSemiring.proof_10.{u, v₁, v₂} R inst A inst_1 inst_2 B inst_3 inst_4) | |
| (@Algebra.TensorProduct.instSemiring.proof_11.{u, v₁, v₂} R inst A inst_1 inst_2 B inst_3 inst_4)) | |
| (@Algebra.TensorProduct.mul_assoc.{u, v₁, v₂} R inst A inst_1 inst_2 B inst_3 inst_4)) | |
| (@One.mk.{max v₁ v₂} | |
| (@TensorProduct.{u, v₁, v₂} R inst A B | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₁} A | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₁} A (@Semiring.toNonAssocSemiring.{v₁} A inst_1))) | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₂} B | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₂} B (@Semiring.toNonAssocSemiring.{v₂} B inst_3))) | |
| (@Algebra.toModule.{u, v₁} R A inst inst_1 inst_2) (@Algebra.toModule.{u, v₂} R B inst inst_3 inst_4)) | |
| (@OfNat.ofNat.{max v₁ v₂} | |
| (@TensorProduct.{u, v₁, v₂} R inst A B | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₁} A | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₁} A (@Semiring.toNonAssocSemiring.{v₁} A inst_1))) | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₂} B | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₂} B (@Semiring.toNonAssocSemiring.{v₂} B inst_3))) | |
| (@Algebra.toModule.{u, v₁} R A inst inst_1 inst_2) (@Algebra.toModule.{u, v₂} R B inst inst_3 inst_4)) | |
| 1 | |
| (@One.toOfNat1.{max v₁ v₂} | |
| (@TensorProduct.{u, v₁, v₂} R inst A B | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₁} A | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₁} A (@Semiring.toNonAssocSemiring.{v₁} A inst_1))) | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₂} B | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₂} B (@Semiring.toNonAssocSemiring.{v₂} B inst_3))) | |
| (@Algebra.toModule.{u, v₁} R A inst inst_1 inst_2) (@Algebra.toModule.{u, v₂} R B inst inst_3 inst_4)) | |
| (@Algebra.TensorProduct.instOneTensorProductToAddCommMonoidToNonUnitalNonAssocSemiringToNonAssocSemiringToAddCommMonoidToNonUnitalNonAssocSemiringToNonAssocSemiringToModuleToModule.{u, | |
| v₁, v₂} | |
| R inst A inst_1 inst_2 B inst_3 inst_4)))) | |
| (@Algebra.TensorProduct.one_mul.{u, v₁, v₂} R inst A inst_1 inst_2 B inst_3 inst_4) | |
| (@Algebra.TensorProduct.mul_one.{u, v₁, v₂} R inst A inst_1 inst_2 B inst_3 inst_4) | |
| (@AddMonoidWithOne.toNatCast.{max v₁ v₂} | |
| (@TensorProduct.{u, v₁, v₂} R inst A B | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₁} A | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₁} A (@Semiring.toNonAssocSemiring.{v₁} A inst_1))) | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₂} B | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₂} B (@Semiring.toNonAssocSemiring.{v₂} B inst_3))) | |
| (@Algebra.toModule.{u, v₁} R A inst inst_1 inst_2) (@Algebra.toModule.{u, v₂} R B inst inst_3 inst_4)) | |
| src) | |
| (@Algebra.TensorProduct.instSemiring.proof_12.{v₁, v₂, u} R inst A inst_1 inst_2 B inst_3 inst_4) | |
| (@Algebra.TensorProduct.instSemiring.proof_13.{v₁, v₂, u} R inst A inst_1 inst_2 B inst_3 inst_4) | |
| (@npowRec.{max v₁ v₂} | |
| (@TensorProduct.{u, v₁, v₂} R inst A B | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₁} A (@Semiring.toNonAssocSemiring.{v₁} A inst_1)).1 | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₂} B (@Semiring.toNonAssocSemiring.{v₂} B inst_3)).1 | |
| (@Algebra.toModule.{u, v₁} R A inst inst_1 inst_2) (@Algebra.toModule.{u, v₂} R B inst inst_3 inst_4)) | |
| (@One.mk.{max v₁ v₂} | |
| (@TensorProduct.{u, v₁, v₂} R inst A B | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₁} A (@Semiring.toNonAssocSemiring.{v₁} A inst_1)).1 | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₂} B (@Semiring.toNonAssocSemiring.{v₂} B inst_3)).1 | |
| (@Algebra.toModule.{u, v₁} R A inst inst_1 inst_2) (@Algebra.toModule.{u, v₂} R B inst inst_3 inst_4)) | |
| (@OfNat.ofNat.{max v₁ v₂} | |
| (@TensorProduct.{u, v₁, v₂} R inst A B | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₁} A (@Semiring.toNonAssocSemiring.{v₁} A inst_1)).1 | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₂} B (@Semiring.toNonAssocSemiring.{v₂} B inst_3)).1 | |
| (@Algebra.toModule.{u, v₁} R A inst inst_1 inst_2) (@Algebra.toModule.{u, v₂} R B inst inst_3 inst_4)) | |
| 1 | |
| (@One.toOfNat1.{max v₁ v₂} | |
| (@TensorProduct.{u, v₁, v₂} R inst A B | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₁} A (@Semiring.toNonAssocSemiring.{v₁} A inst_1)).1 | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₂} B (@Semiring.toNonAssocSemiring.{v₂} B inst_3)).1 | |
| (@Algebra.toModule.{u, v₁} R A inst inst_1 inst_2) (@Algebra.toModule.{u, v₂} R B inst inst_3 inst_4)) | |
| (@Algebra.TensorProduct.instOneTensorProductToAddCommMonoidToNonUnitalNonAssocSemiringToNonAssocSemiringToAddCommMonoidToNonUnitalNonAssocSemiringToNonAssocSemiringToModuleToModule.{u, | |
| v₁, v₂} | |
| R inst A inst_1 inst_2 B inst_3 inst_4)))) | |
| (@Mul.mk.{max v₁ v₂} | |
| (@TensorProduct.{u, v₁, v₂} R inst A B | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₁} A (@Semiring.toNonAssocSemiring.{v₁} A inst_1)).1 | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₂} B (@Semiring.toNonAssocSemiring.{v₂} B inst_3)).1 | |
| (@Algebra.toModule.{u, v₁} R A inst inst_1 inst_2) (@Algebra.toModule.{u, v₂} R B inst inst_3 inst_4)) | |
| fun | |
| (a b : | |
| @TensorProduct.{u, v₁, v₂} R inst A B | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₁} A | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₁} A (@Semiring.toNonAssocSemiring.{v₁} A inst_1))) | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₂} B | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₂} B (@Semiring.toNonAssocSemiring.{v₂} B inst_3))) | |
| (@Algebra.toModule.{u, v₁} R A inst inst_1 inst_2) (@Algebra.toModule.{u, v₂} R B inst inst_3 inst_4)) ↦ | |
| @FunLike.coe.{max (v₁ + 1) (v₂ + 1), max (v₁ + 1) (v₂ + 1), max (v₁ + 1) (v₂ + 1)} | |
| (@LinearMap.{u, u, max v₂ v₁, max v₂ v₁} R R (@CommSemiring.toSemiring.{u} R inst) | |
| (@CommSemiring.toSemiring.{u} R inst) | |
| (@RingHom.id.{u} R (@Semiring.toNonAssocSemiring.{u} R (@CommSemiring.toSemiring.{u} R inst))) | |
| (@TensorProduct.{u, v₁, v₂} R inst A B | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₁} A (@Semiring.toNonAssocSemiring.{v₁} A inst_1)).1 | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₂} B (@Semiring.toNonAssocSemiring.{v₂} B inst_3)).1 | |
| (@Algebra.toModule.{u, v₁} R A inst inst_1 inst_2) (@Algebra.toModule.{u, v₂} R B inst inst_3 inst_4)) | |
| (@TensorProduct.{u, v₁, v₂} R inst A B | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₁} A (@Semiring.toNonAssocSemiring.{v₁} A inst_1)).1 | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₂} B (@Semiring.toNonAssocSemiring.{v₂} B inst_3)).1 | |
| (@Algebra.toModule.{u, v₁} R A inst inst_1 inst_2) (@Algebra.toModule.{u, v₂} R B inst inst_3 inst_4)) | |
| (@TensorProduct.addCommMonoid.{u, v₁, v₂} R inst A B | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₁} A (@Semiring.toNonAssocSemiring.{v₁} A inst_1)).1 | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₂} B (@Semiring.toNonAssocSemiring.{v₂} B inst_3)).1 | |
| (@Algebra.toModule.{u, v₁} R A inst inst_1 inst_2) (@Algebra.toModule.{u, v₂} R B inst inst_3 inst_4)) | |
| (@TensorProduct.addCommMonoid.{u, v₁, v₂} R inst A B | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₁} A (@Semiring.toNonAssocSemiring.{v₁} A inst_1)).1 | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₂} B (@Semiring.toNonAssocSemiring.{v₂} B inst_3)).1 | |
| (@Algebra.toModule.{u, v₁} R A inst inst_1 inst_2) (@Algebra.toModule.{u, v₂} R B inst inst_3 inst_4)) | |
| (@TensorProduct.instModuleTensorProductToSemiringAddCommMonoid.{u, v₁, v₂} R inst A B | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₁} A (@Semiring.toNonAssocSemiring.{v₁} A inst_1)).1 | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₂} B (@Semiring.toNonAssocSemiring.{v₂} B inst_3)).1 | |
| (@Algebra.toModule.{u, v₁} R A inst inst_1 inst_2) (@Algebra.toModule.{u, v₂} R B inst inst_3 inst_4)) | |
| (@TensorProduct.instModuleTensorProductToSemiringAddCommMonoid.{u, v₁, v₂} R inst A B | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₁} A (@Semiring.toNonAssocSemiring.{v₁} A inst_1)).1 | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₂} B (@Semiring.toNonAssocSemiring.{v₂} B inst_3)).1 | |
| (@Algebra.toModule.{u, v₁} R A inst inst_1 inst_2) (@Algebra.toModule.{u, v₂} R B inst inst_3 inst_4))) | |
| (@TensorProduct.{u, v₁, v₂} R inst A B | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₁} A (@Semiring.toNonAssocSemiring.{v₁} A inst_1)).1 | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₂} B (@Semiring.toNonAssocSemiring.{v₂} B inst_3)).1 | |
| (@Algebra.toModule.{u, v₁} R A inst inst_1 inst_2) (@Algebra.toModule.{u, v₂} R B inst inst_3 inst_4)) | |
| (fun | |
| (a : | |
| @TensorProduct.{u, v₁, v₂} R inst A B | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₁} A | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₁} A (@Semiring.toNonAssocSemiring.{v₁} A inst_1))) | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₂} B | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₂} B (@Semiring.toNonAssocSemiring.{v₂} B inst_3))) | |
| (@Algebra.toModule.{u, v₁} R A inst inst_1 inst_2) | |
| (@Algebra.toModule.{u, v₂} R B inst inst_3 inst_4)) ↦ | |
| @TensorProduct.{u, v₁, v₂} R inst A B | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₁} A (@Semiring.toNonAssocSemiring.{v₁} A inst_1)).1 | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₂} B (@Semiring.toNonAssocSemiring.{v₂} B inst_3)).1 | |
| (@Algebra.toModule.{u, v₁} R A inst inst_1 inst_2) (@Algebra.toModule.{u, v₂} R B inst inst_3 inst_4)) | |
| (@LinearMap.instFunLikeLinearMap.{u, u, max v₁ v₂, max v₁ v₂} R R | |
| (@TensorProduct.{u, v₁, v₂} R inst A B | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₁} A (@Semiring.toNonAssocSemiring.{v₁} A inst_1)).1 | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₂} B (@Semiring.toNonAssocSemiring.{v₂} B inst_3)).1 | |
| (@Algebra.toModule.{u, v₁} R A inst inst_1 inst_2) (@Algebra.toModule.{u, v₂} R B inst inst_3 inst_4)) | |
| (@TensorProduct.{u, v₁, v₂} R inst A B | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₁} A (@Semiring.toNonAssocSemiring.{v₁} A inst_1)).1 | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₂} B (@Semiring.toNonAssocSemiring.{v₂} B inst_3)).1 | |
| (@Algebra.toModule.{u, v₁} R A inst inst_1 inst_2) (@Algebra.toModule.{u, v₂} R B inst inst_3 inst_4)) | |
| (@CommSemiring.toSemiring.{u} R inst) (@CommSemiring.toSemiring.{u} R inst) | |
| (@TensorProduct.addCommMonoid.{u, v₁, v₂} R inst A B | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₁} A (@Semiring.toNonAssocSemiring.{v₁} A inst_1)).1 | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₂} B (@Semiring.toNonAssocSemiring.{v₂} B inst_3)).1 | |
| (@Algebra.toModule.{u, v₁} R A inst inst_1 inst_2) (@Algebra.toModule.{u, v₂} R B inst inst_3 inst_4)) | |
| (@TensorProduct.addCommMonoid.{u, v₁, v₂} R inst A B | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₁} A (@Semiring.toNonAssocSemiring.{v₁} A inst_1)).1 | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₂} B (@Semiring.toNonAssocSemiring.{v₂} B inst_3)).1 | |
| (@Algebra.toModule.{u, v₁} R A inst inst_1 inst_2) (@Algebra.toModule.{u, v₂} R B inst inst_3 inst_4)) | |
| (@TensorProduct.instModuleTensorProductToSemiringAddCommMonoid.{u, v₁, v₂} R inst A B | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₁} A (@Semiring.toNonAssocSemiring.{v₁} A inst_1)).1 | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₂} B (@Semiring.toNonAssocSemiring.{v₂} B inst_3)).1 | |
| (@Algebra.toModule.{u, v₁} R A inst inst_1 inst_2) (@Algebra.toModule.{u, v₂} R B inst inst_3 inst_4)) | |
| (@TensorProduct.instModuleTensorProductToSemiringAddCommMonoid.{u, v₁, v₂} R inst A B | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₁} A (@Semiring.toNonAssocSemiring.{v₁} A inst_1)).1 | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₂} B (@Semiring.toNonAssocSemiring.{v₂} B inst_3)).1 | |
| (@Algebra.toModule.{u, v₁} R A inst inst_1 inst_2) (@Algebra.toModule.{u, v₂} R B inst inst_3 inst_4)) | |
| (@RingHom.id.{u} R (@Semiring.toNonAssocSemiring.{u} R (@CommSemiring.toSemiring.{u} R inst)))) | |
| (@FunLike.coe.{max (v₂ + 1) (v₁ + 1), max (v₂ + 1) (v₁ + 1), max (v₂ + 1) (v₁ + 1)} | |
| (@LinearMap.{u, u, max v₂ v₁, max v₂ v₁} R R (@CommSemiring.toSemiring.{u} R inst) | |
| (@CommSemiring.toSemiring.{u} R inst) | |
| (@RingHom.id.{u} R (@Semiring.toNonAssocSemiring.{u} R (@CommSemiring.toSemiring.{u} R inst))) | |
| (@TensorProduct.{u, v₁, v₂} R inst A B | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₁} A (@Semiring.toNonAssocSemiring.{v₁} A inst_1)).1 | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₂} B (@Semiring.toNonAssocSemiring.{v₂} B inst_3)).1 | |
| (@Algebra.toModule.{u, v₁} R A inst inst_1 inst_2) (@Algebra.toModule.{u, v₂} R B inst inst_3 inst_4)) | |
| (@LinearMap.{u, u, max v₂ v₁, max v₂ v₁} R R (@CommSemiring.toSemiring.{u} R inst) | |
| (@CommSemiring.toSemiring.{u} R inst) | |
| (@RingHom.id.{u} R (@Semiring.toNonAssocSemiring.{u} R (@CommSemiring.toSemiring.{u} R inst))) | |
| (@TensorProduct.{u, v₁, v₂} R inst A B | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₁} A (@Semiring.toNonAssocSemiring.{v₁} A inst_1)).1 | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₂} B (@Semiring.toNonAssocSemiring.{v₂} B inst_3)).1 | |
| (@Algebra.toModule.{u, v₁} R A inst inst_1 inst_2) (@Algebra.toModule.{u, v₂} R B inst inst_3 inst_4)) | |
| (@TensorProduct.{u, v₁, v₂} R inst A B | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₁} A (@Semiring.toNonAssocSemiring.{v₁} A inst_1)).1 | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₂} B (@Semiring.toNonAssocSemiring.{v₂} B inst_3)).1 | |
| (@Algebra.toModule.{u, v₁} R A inst inst_1 inst_2) (@Algebra.toModule.{u, v₂} R B inst inst_3 inst_4)) | |
| (@TensorProduct.addCommMonoid.{u, v₁, v₂} R inst A B | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₁} A (@Semiring.toNonAssocSemiring.{v₁} A inst_1)).1 | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₂} B (@Semiring.toNonAssocSemiring.{v₂} B inst_3)).1 | |
| (@Algebra.toModule.{u, v₁} R A inst inst_1 inst_2) (@Algebra.toModule.{u, v₂} R B inst inst_3 inst_4)) | |
| (@TensorProduct.addCommMonoid.{u, v₁, v₂} R inst A B | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₁} A (@Semiring.toNonAssocSemiring.{v₁} A inst_1)).1 | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₂} B (@Semiring.toNonAssocSemiring.{v₂} B inst_3)).1 | |
| (@Algebra.toModule.{u, v₁} R A inst inst_1 inst_2) (@Algebra.toModule.{u, v₂} R B inst inst_3 inst_4)) | |
| (@TensorProduct.instModuleTensorProductToSemiringAddCommMonoid.{u, v₁, v₂} R inst A B | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₁} A (@Semiring.toNonAssocSemiring.{v₁} A inst_1)).1 | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₂} B (@Semiring.toNonAssocSemiring.{v₂} B inst_3)).1 | |
| (@Algebra.toModule.{u, v₁} R A inst inst_1 inst_2) (@Algebra.toModule.{u, v₂} R B inst inst_3 inst_4)) | |
| (@TensorProduct.instModuleTensorProductToSemiringAddCommMonoid.{u, v₁, v₂} R inst A B | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₁} A (@Semiring.toNonAssocSemiring.{v₁} A inst_1)).1 | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₂} B (@Semiring.toNonAssocSemiring.{v₂} B inst_3)).1 | |
| (@Algebra.toModule.{u, v₁} R A inst inst_1 inst_2) | |
| (@Algebra.toModule.{u, v₂} R B inst inst_3 inst_4))) | |
| (@TensorProduct.addCommMonoid.{u, v₁, v₂} R inst A B | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₁} A (@Semiring.toNonAssocSemiring.{v₁} A inst_1)).1 | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₂} B (@Semiring.toNonAssocSemiring.{v₂} B inst_3)).1 | |
| (@Algebra.toModule.{u, v₁} R A inst inst_1 inst_2) (@Algebra.toModule.{u, v₂} R B inst inst_3 inst_4)) | |
| (@LinearMap.addCommMonoid.{u, u, max v₁ v₂, max v₁ v₂} R R | |
| (@TensorProduct.{u, v₁, v₂} R inst A B | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₁} A (@Semiring.toNonAssocSemiring.{v₁} A inst_1)).1 | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₂} B (@Semiring.toNonAssocSemiring.{v₂} B inst_3)).1 | |
| (@Algebra.toModule.{u, v₁} R A inst inst_1 inst_2) (@Algebra.toModule.{u, v₂} R B inst inst_3 inst_4)) | |
| (@TensorProduct.{u, v₁, v₂} R inst A B | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₁} A (@Semiring.toNonAssocSemiring.{v₁} A inst_1)).1 | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₂} B (@Semiring.toNonAssocSemiring.{v₂} B inst_3)).1 | |
| (@Algebra.toModule.{u, v₁} R A inst inst_1 inst_2) (@Algebra.toModule.{u, v₂} R B inst inst_3 inst_4)) | |
| (@CommSemiring.toSemiring.{u} R inst) (@CommSemiring.toSemiring.{u} R inst) | |
| (@TensorProduct.addCommMonoid.{u, v₁, v₂} R inst A B | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₁} A (@Semiring.toNonAssocSemiring.{v₁} A inst_1)).1 | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₂} B (@Semiring.toNonAssocSemiring.{v₂} B inst_3)).1 | |
| (@Algebra.toModule.{u, v₁} R A inst inst_1 inst_2) (@Algebra.toModule.{u, v₂} R B inst inst_3 inst_4)) | |
| (@TensorProduct.addCommMonoid.{u, v₁, v₂} R inst A B | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₁} A (@Semiring.toNonAssocSemiring.{v₁} A inst_1)).1 | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₂} B (@Semiring.toNonAssocSemiring.{v₂} B inst_3)).1 | |
| (@Algebra.toModule.{u, v₁} R A inst inst_1 inst_2) (@Algebra.toModule.{u, v₂} R B inst inst_3 inst_4)) | |
| (@TensorProduct.instModuleTensorProductToSemiringAddCommMonoid.{u, v₁, v₂} R inst A B | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₁} A (@Semiring.toNonAssocSemiring.{v₁} A inst_1)).1 | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₂} B (@Semiring.toNonAssocSemiring.{v₂} B inst_3)).1 | |
| (@Algebra.toModule.{u, v₁} R A inst inst_1 inst_2) (@Algebra.toModule.{u, v₂} R B inst inst_3 inst_4)) | |
| (@TensorProduct.instModuleTensorProductToSemiringAddCommMonoid.{u, v₁, v₂} R inst A B | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₁} A (@Semiring.toNonAssocSemiring.{v₁} A inst_1)).1 | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₂} B (@Semiring.toNonAssocSemiring.{v₂} B inst_3)).1 | |
| (@Algebra.toModule.{u, v₁} R A inst inst_1 inst_2) (@Algebra.toModule.{u, v₂} R B inst inst_3 inst_4)) | |
| (@RingHom.id.{u} R (@Semiring.toNonAssocSemiring.{u} R (@CommSemiring.toSemiring.{u} R inst)))) | |
| (@TensorProduct.instModuleTensorProductToSemiringAddCommMonoid.{u, v₁, v₂} R inst A B | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₁} A (@Semiring.toNonAssocSemiring.{v₁} A inst_1)).1 | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₂} B (@Semiring.toNonAssocSemiring.{v₂} B inst_3)).1 | |
| (@Algebra.toModule.{u, v₁} R A inst inst_1 inst_2) (@Algebra.toModule.{u, v₂} R B inst inst_3 inst_4)) | |
| (@LinearMap.module.{u, u, u, max v₁ v₂, max v₁ v₂} R R R | |
| (@TensorProduct.{u, v₁, v₂} R inst A B | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₁} A (@Semiring.toNonAssocSemiring.{v₁} A inst_1)).1 | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₂} B (@Semiring.toNonAssocSemiring.{v₂} B inst_3)).1 | |
| (@Algebra.toModule.{u, v₁} R A inst inst_1 inst_2) (@Algebra.toModule.{u, v₂} R B inst inst_3 inst_4)) | |
| (@TensorProduct.{u, v₁, v₂} R inst A B | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₁} A (@Semiring.toNonAssocSemiring.{v₁} A inst_1)).1 | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₂} B (@Semiring.toNonAssocSemiring.{v₂} B inst_3)).1 | |
| (@Algebra.toModule.{u, v₁} R A inst inst_1 inst_2) (@Algebra.toModule.{u, v₂} R B inst inst_3 inst_4)) | |
| (@CommSemiring.toSemiring.{u} R inst) (@CommSemiring.toSemiring.{u} R inst) | |
| (@TensorProduct.addCommMonoid.{u, v₁, v₂} R inst A B | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₁} A (@Semiring.toNonAssocSemiring.{v₁} A inst_1)).1 | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₂} B (@Semiring.toNonAssocSemiring.{v₂} B inst_3)).1 | |
| (@Algebra.toModule.{u, v₁} R A inst inst_1 inst_2) (@Algebra.toModule.{u, v₂} R B inst inst_3 inst_4)) | |
| (@TensorProduct.addCommMonoid.{u, v₁, v₂} R inst A B | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₁} A (@Semiring.toNonAssocSemiring.{v₁} A inst_1)).1 | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₂} B (@Semiring.toNonAssocSemiring.{v₂} B inst_3)).1 | |
| (@Algebra.toModule.{u, v₁} R A inst inst_1 inst_2) (@Algebra.toModule.{u, v₂} R B inst inst_3 inst_4)) | |
| (@TensorProduct.instModuleTensorProductToSemiringAddCommMonoid.{u, v₁, v₂} R inst A B | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₁} A (@Semiring.toNonAssocSemiring.{v₁} A inst_1)).1 | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₂} B (@Semiring.toNonAssocSemiring.{v₂} B inst_3)).1 | |
| (@Algebra.toModule.{u, v₁} R A inst inst_1 inst_2) (@Algebra.toModule.{u, v₂} R B inst inst_3 inst_4)) | |
| (@TensorProduct.instModuleTensorProductToSemiringAddCommMonoid.{u, v₁, v₂} R inst A B | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₁} A (@Semiring.toNonAssocSemiring.{v₁} A inst_1)).1 | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₂} B (@Semiring.toNonAssocSemiring.{v₂} B inst_3)).1 | |
| (@Algebra.toModule.{u, v₁} R A inst inst_1 inst_2) (@Algebra.toModule.{u, v₂} R B inst inst_3 inst_4)) | |
| (@RingHom.id.{u} R (@Semiring.toNonAssocSemiring.{u} R (@CommSemiring.toSemiring.{u} R inst))) | |
| (@CommSemiring.toSemiring.{u} R inst) | |
| (@TensorProduct.instModuleTensorProductToSemiringAddCommMonoid.{u, v₁, v₂} R inst A B | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₁} A (@Semiring.toNonAssocSemiring.{v₁} A inst_1)).1 | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₂} B (@Semiring.toNonAssocSemiring.{v₂} B inst_3)).1 | |
| (@Algebra.toModule.{u, v₁} R A inst inst_1 inst_2) (@Algebra.toModule.{u, v₂} R B inst inst_3 inst_4)) | |
| (@Algebra.TensorProduct.instSemiring.proof_14.{u, v₁, v₂} R inst A inst_1 inst_2 B inst_3 inst_4))) | |
| (@TensorProduct.{u, v₁, v₂} R inst A B | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₁} A (@Semiring.toNonAssocSemiring.{v₁} A inst_1)).1 | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₂} B (@Semiring.toNonAssocSemiring.{v₂} B inst_3)).1 | |
| (@Algebra.toModule.{u, v₁} R A inst inst_1 inst_2) (@Algebra.toModule.{u, v₂} R B inst inst_3 inst_4)) | |
| (fun | |
| (a : | |
| @TensorProduct.{u, v₁, v₂} R inst A B | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₁} A | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₁} A | |
| (@Semiring.toNonAssocSemiring.{v₁} A inst_1))) | |
| (@NonUnitalNonAssocSemiring.toAddCommMonoid.{v₂} B | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₂} B | |
| (@Semiring.toNonAssocSemiring.{v₂} B inst_3))) | |
| (@Algebra.toModule.{u, v₁} R A inst inst_1 inst_2) | |
| (@Algebra.toModule.{u, v₂} R B inst inst_3 inst_4)) ↦ | |
| @LinearMap.{u, u, max v₂ v₁, max v₂ v₁} R R (@CommSemiring.toSemiring.{u} R inst) | |
| (@CommSemiring.toSemiring.{u} R inst) | |
| (@RingHom.id.{u} R (@Semiring.toNonAssocSemiring.{u} R (@CommSemiring.toSemiring.{u} R inst))) | |
| (@TensorProduct.{u, v₁, v₂} R inst A B | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₁} A (@Semiring.toNonAssocSemiring.{v₁} A inst_1)).1 | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₂} B (@Semiring.toNonAssocSemiring.{v₂} B inst_3)).1 | |
| (@Algebra.toModule.{u, v₁} R A inst inst_1 inst_2) (@Algebra.toModule.{u, v₂} R B inst inst_3 inst_4)) | |
| (@TensorProduct.{u, v₁, v₂} R inst A B | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₁} A (@Semiring.toNonAssocSemiring.{v₁} A inst_1)).1 | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₂} B (@Semiring.toNonAssocSemiring.{v₂} B inst_3)).1 | |
| (@Algebra.toModule.{u, v₁} R A inst inst_1 inst_2) (@Algebra.toModule.{u, v₂} R B inst inst_3 inst_4)) | |
| (@TensorProduct.addCommMonoid.{u, v₁, v₂} R inst A B | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₁} A (@Semiring.toNonAssocSemiring.{v₁} A inst_1)).1 | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₂} B (@Semiring.toNonAssocSemiring.{v₂} B inst_3)).1 | |
| (@Algebra.toModule.{u, v₁} R A inst inst_1 inst_2) (@Algebra.toModule.{u, v₂} R B inst inst_3 inst_4)) | |
| (@TensorProduct.addCommMonoid.{u, v₁, v₂} R inst A B | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₁} A (@Semiring.toNonAssocSemiring.{v₁} A inst_1)).1 | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₂} B (@Semiring.toNonAssocSemiring.{v₂} B inst_3)).1 | |
| (@Algebra.toModule.{u, v₁} R A inst inst_1 inst_2) (@Algebra.toModule.{u, v₂} R B inst inst_3 inst_4)) | |
| (@TensorProduct.instModuleTensorProductToSemiringAddCommMonoid.{u, v₁, v₂} R inst A B | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₁} A (@Semiring.toNonAssocSemiring.{v₁} A inst_1)).1 | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₂} B (@Semiring.toNonAssocSemiring.{v₂} B inst_3)).1 | |
| (@Algebra.toModule.{u, v₁} R A inst inst_1 inst_2) (@Algebra.toModule.{u, v₂} R B inst inst_3 inst_4)) | |
| (@TensorProduct.instModuleTensorProductToSemiringAddCommMonoid.{u, v₁, v₂} R inst A B | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₁} A (@Semiring.toNonAssocSemiring.{v₁} A inst_1)).1 | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₂} B (@Semiring.toNonAssocSemiring.{v₂} B inst_3)).1 | |
| (@Algebra.toModule.{u, v₁} R A inst inst_1 inst_2) | |
| (@Algebra.toModule.{u, v₂} R B inst inst_3 inst_4))) | |
| (@LinearMap.instFunLikeLinearMap.{u, u, max v₂ v₁, max v₂ v₁} R R | |
| (@TensorProduct.{u, v₁, v₂} R inst A B | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₁} A (@Semiring.toNonAssocSemiring.{v₁} A inst_1)).1 | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₂} B (@Semiring.toNonAssocSemiring.{v₂} B inst_3)).1 | |
| (@Algebra.toModule.{u, v₁} R A inst inst_1 inst_2) (@Algebra.toModule.{u, v₂} R B inst inst_3 inst_4)) | |
| (@LinearMap.{u, u, max v₂ v₁, max v₂ v₁} R R (@CommSemiring.toSemiring.{u} R inst) | |
| (@CommSemiring.toSemiring.{u} R inst) | |
| (@RingHom.id.{u} R (@Semiring.toNonAssocSemiring.{u} R (@CommSemiring.toSemiring.{u} R inst))) | |
| (@TensorProduct.{u, v₁, v₂} R inst A B | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₁} A (@Semiring.toNonAssocSemiring.{v₁} A inst_1)).1 | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₂} B (@Semiring.toNonAssocSemiring.{v₂} B inst_3)).1 | |
| (@Algebra.toModule.{u, v₁} R A inst inst_1 inst_2) (@Algebra.toModule.{u, v₂} R B inst inst_3 inst_4)) | |
| (@TensorProduct.{u, v₁, v₂} R inst A B | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₁} A (@Semiring.toNonAssocSemiring.{v₁} A inst_1)).1 | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₂} B (@Semiring.toNonAssocSemiring.{v₂} B inst_3)).1 | |
| (@Algebra.toModule.{u, v₁} R A inst inst_1 inst_2) (@Algebra.toModule.{u, v₂} R B inst inst_3 inst_4)) | |
| (@TensorProduct.addCommMonoid.{u, v₁, v₂} R inst A B | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₁} A (@Semiring.toNonAssocSemiring.{v₁} A inst_1)).1 | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₂} B (@Semiring.toNonAssocSemiring.{v₂} B inst_3)).1 | |
| (@Algebra.toModule.{u, v₁} R A inst inst_1 inst_2) (@Algebra.toModule.{u, v₂} R B inst inst_3 inst_4)) | |
| (@TensorProduct.addCommMonoid.{u, v₁, v₂} R inst A B | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₁} A (@Semiring.toNonAssocSemiring.{v₁} A inst_1)).1 | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₂} B (@Semiring.toNonAssocSemiring.{v₂} B inst_3)).1 | |
| (@Algebra.toModule.{u, v₁} R A inst inst_1 inst_2) (@Algebra.toModule.{u, v₂} R B inst inst_3 inst_4)) | |
| (@TensorProduct.instModuleTensorProductToSemiringAddCommMonoid.{u, v₁, v₂} R inst A B | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₁} A (@Semiring.toNonAssocSemiring.{v₁} A inst_1)).1 | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₂} B (@Semiring.toNonAssocSemiring.{v₂} B inst_3)).1 | |
| (@Algebra.toModule.{u, v₁} R A inst inst_1 inst_2) (@Algebra.toModule.{u, v₂} R B inst inst_3 inst_4)) | |
| (@TensorProduct.instModuleTensorProductToSemiringAddCommMonoid.{u, v₁, v₂} R inst A B | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₁} A (@Semiring.toNonAssocSemiring.{v₁} A inst_1)).1 | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₂} B (@Semiring.toNonAssocSemiring.{v₂} B inst_3)).1 | |
| (@Algebra.toModule.{u, v₁} R A inst inst_1 inst_2) | |
| (@Algebra.toModule.{u, v₂} R B inst inst_3 inst_4))) | |
| (@CommSemiring.toSemiring.{u} R inst) (@CommSemiring.toSemiring.{u} R inst) | |
| (@TensorProduct.addCommMonoid.{u, v₁, v₂} R inst A B | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₁} A (@Semiring.toNonAssocSemiring.{v₁} A inst_1)).1 | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₂} B (@Semiring.toNonAssocSemiring.{v₂} B inst_3)).1 | |
| (@Algebra.toModule.{u, v₁} R A inst inst_1 inst_2) (@Algebra.toModule.{u, v₂} R B inst inst_3 inst_4)) | |
| (@LinearMap.addCommMonoid.{u, u, max v₁ v₂, max v₁ v₂} R R | |
| (@TensorProduct.{u, v₁, v₂} R inst A B | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₁} A (@Semiring.toNonAssocSemiring.{v₁} A inst_1)).1 | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₂} B (@Semiring.toNonAssocSemiring.{v₂} B inst_3)).1 | |
| (@Algebra.toModule.{u, v₁} R A inst inst_1 inst_2) (@Algebra.toModule.{u, v₂} R B inst inst_3 inst_4)) | |
| (@TensorProduct.{u, v₁, v₂} R inst A B | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₁} A (@Semiring.toNonAssocSemiring.{v₁} A inst_1)).1 | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₂} B (@Semiring.toNonAssocSemiring.{v₂} B inst_3)).1 | |
| (@Algebra.toModule.{u, v₁} R A inst inst_1 inst_2) (@Algebra.toModule.{u, v₂} R B inst inst_3 inst_4)) | |
| (@CommSemiring.toSemiring.{u} R inst) (@CommSemiring.toSemiring.{u} R inst) | |
| (@TensorProduct.addCommMonoid.{u, v₁, v₂} R inst A B | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₁} A (@Semiring.toNonAssocSemiring.{v₁} A inst_1)).1 | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₂} B (@Semiring.toNonAssocSemiring.{v₂} B inst_3)).1 | |
| (@Algebra.toModule.{u, v₁} R A inst inst_1 inst_2) (@Algebra.toModule.{u, v₂} R B inst inst_3 inst_4)) | |
| (@TensorProduct.addCommMonoid.{u, v₁, v₂} R inst A B | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₁} A (@Semiring.toNonAssocSemiring.{v₁} A inst_1)).1 | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₂} B (@Semiring.toNonAssocSemiring.{v₂} B inst_3)).1 | |
| (@Algebra.toModule.{u, v₁} R A inst inst_1 inst_2) (@Algebra.toModule.{u, v₂} R B inst inst_3 inst_4)) | |
| (@TensorProduct.instModuleTensorProductToSemiringAddCommMonoid.{u, v₁, v₂} R inst A B | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₁} A (@Semiring.toNonAssocSemiring.{v₁} A inst_1)).1 | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₂} B (@Semiring.toNonAssocSemiring.{v₂} B inst_3)).1 | |
| (@Algebra.toModule.{u, v₁} R A inst inst_1 inst_2) (@Algebra.toModule.{u, v₂} R B inst inst_3 inst_4)) | |
| (@TensorProduct.instModuleTensorProductToSemiringAddCommMonoid.{u, v₁, v₂} R inst A B | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₁} A (@Semiring.toNonAssocSemiring.{v₁} A inst_1)).1 | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₂} B (@Semiring.toNonAssocSemiring.{v₂} B inst_3)).1 | |
| (@Algebra.toModule.{u, v₁} R A inst inst_1 inst_2) (@Algebra.toModule.{u, v₂} R B inst inst_3 inst_4)) | |
| (@RingHom.id.{u} R (@Semiring.toNonAssocSemiring.{u} R (@CommSemiring.toSemiring.{u} R inst)))) | |
| (@TensorProduct.instModuleTensorProductToSemiringAddCommMonoid.{u, v₁, v₂} R inst A B | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₁} A (@Semiring.toNonAssocSemiring.{v₁} A inst_1)).1 | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₂} B (@Semiring.toNonAssocSemiring.{v₂} B inst_3)).1 | |
| (@Algebra.toModule.{u, v₁} R A inst inst_1 inst_2) (@Algebra.toModule.{u, v₂} R B inst inst_3 inst_4)) | |
| (@LinearMap.module.{u, u, u, max v₁ v₂, max v₁ v₂} R R R | |
| (@TensorProduct.{u, v₁, v₂} R inst A B | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₁} A (@Semiring.toNonAssocSemiring.{v₁} A inst_1)).1 | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₂} B (@Semiring.toNonAssocSemiring.{v₂} B inst_3)).1 | |
| (@Algebra.toModule.{u, v₁} R A inst inst_1 inst_2) (@Algebra.toModule.{u, v₂} R B inst inst_3 inst_4)) | |
| (@TensorProduct.{u, v₁, v₂} R inst A B | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₁} A (@Semiring.toNonAssocSemiring.{v₁} A inst_1)).1 | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₂} B (@Semiring.toNonAssocSemiring.{v₂} B inst_3)).1 | |
| (@Algebra.toModule.{u, v₁} R A inst inst_1 inst_2) (@Algebra.toModule.{u, v₂} R B inst inst_3 inst_4)) | |
| (@CommSemiring.toSemiring.{u} R inst) (@CommSemiring.toSemiring.{u} R inst) | |
| (@TensorProduct.addCommMonoid.{u, v₁, v₂} R inst A B | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₁} A (@Semiring.toNonAssocSemiring.{v₁} A inst_1)).1 | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₂} B (@Semiring.toNonAssocSemiring.{v₂} B inst_3)).1 | |
| (@Algebra.toModule.{u, v₁} R A inst inst_1 inst_2) (@Algebra.toModule.{u, v₂} R B inst inst_3 inst_4)) | |
| (@TensorProduct.addCommMonoid.{u, v₁, v₂} R inst A B | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₁} A (@Semiring.toNonAssocSemiring.{v₁} A inst_1)).1 | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₂} B (@Semiring.toNonAssocSemiring.{v₂} B inst_3)).1 | |
| (@Algebra.toModule.{u, v₁} R A inst inst_1 inst_2) (@Algebra.toModule.{u, v₂} R B inst inst_3 inst_4)) | |
| (@TensorProduct.instModuleTensorProductToSemiringAddCommMonoid.{u, v₁, v₂} R inst A B | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₁} A (@Semiring.toNonAssocSemiring.{v₁} A inst_1)).1 | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₂} B (@Semiring.toNonAssocSemiring.{v₂} B inst_3)).1 | |
| (@Algebra.toModule.{u, v₁} R A inst inst_1 inst_2) (@Algebra.toModule.{u, v₂} R B inst inst_3 inst_4)) | |
| (@TensorProduct.instModuleTensorProductToSemiringAddCommMonoid.{u, v₁, v₂} R inst A B | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₁} A (@Semiring.toNonAssocSemiring.{v₁} A inst_1)).1 | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₂} B (@Semiring.toNonAssocSemiring.{v₂} B inst_3)).1 | |
| (@Algebra.toModule.{u, v₁} R A inst inst_1 inst_2) (@Algebra.toModule.{u, v₂} R B inst inst_3 inst_4)) | |
| (@RingHom.id.{u} R (@Semiring.toNonAssocSemiring.{u} R (@CommSemiring.toSemiring.{u} R inst))) | |
| (@CommSemiring.toSemiring.{u} R inst) | |
| (@TensorProduct.instModuleTensorProductToSemiringAddCommMonoid.{u, v₁, v₂} R inst A B | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₁} A (@Semiring.toNonAssocSemiring.{v₁} A inst_1)).1 | |
| (@NonAssocSemiring.toNonUnitalNonAssocSemiring.{v₂} B (@Semiring.toNonAssocSemiring.{v₂} B inst_3)).1 | |
| (@Algebra.toModule.{u, v₁} R A inst inst_1 inst_2) (@Algebra.toModule.{u, v₂} R B inst inst_3 inst_4)) | |
| (@Algebra.TensorProduct.instSemiring.proof_14.{u, v₁, v₂} R inst A inst_1 inst_2 B inst_3 inst_4)) | |
| (@RingHom.id.{u} R (@Semiring.toNonAssocSemiring.{u} R (@CommSemiring.toSemiring.{u} R inst)))) | |
| (@Algebra.TensorProduct.mul.{u, v₁, v₂} R inst A inst_1 inst_2 B inst_3 inst_4) a) | |
| b)) | |
| (@Algebra.TensorProduct.instSemiring.proof_15.{u, v₁, v₂} R inst A inst_1 inst_2 B inst_3 inst_4) | |
| (@Algebra.TensorProduct.instSemiring.proof_16.{u, v₁, v₂} R inst A inst_1 inst_2 B inst_3 inst_4) |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment