Revision #2621 → #3188 · back to history
modifiedOuter product of tensors (lead)ca1360a84c55
| Field | From #2621 | To #3188 |
|---|
| mathlib.module | Mathlib.LinearAlgebra.TensorProduct.Basic | Mathlib.LinearAlgebra.TensorProduct.Defs |
modifiedOuter product of tensors28657a953e6b
| Field | From #2621 | To #3188 |
|---|
| mathlib.module | Mathlib.LinearAlgebra.TensorProduct.Basic | Mathlib.LinearAlgebra.TensorProduct.Defs |
modifiedAssociativity of tensor outer product846437c3fea1
| Field | From #2621 | To #3188 |
|---|
| mathlib.module | Mathlib.LinearAlgebra.TensorProduct.Basic | Mathlib.LinearAlgebra.TensorProduct.Associator |
modifiedAbstract outer product84b32917b35f
| Field | From #2621 | To #3188 |
|---|
| mathlib.module | Mathlib.LinearAlgebra.TensorProduct.Basic | Mathlib.LinearAlgebra.TensorProduct.Defs |