Revision #3192 → #3702 · back to history
modifiedTensor product of two vector spacesabc496e326a7
| Field | From #3192 | To #3702 |
|---|
| note | Mathlib defines `TensorProduct R M N` for modules over a commutative semiring, which subsumes the vector-space case. | Mathlib defines `TensorProduct R M N` for modules over a commutative semiring, subsuming the vector-space case. |
modifiedTensor product from bases40ebd6614177
| Field | From #3192 | To #3702 |
|---|
| note | `Basis.tensorProduct` builds a basis of `M ⊗ N` from bases of `M` and `N`. | `Module.Basis.tensorProduct` builds a basis of `M ⊗ N` from bases of `M` and `N`. |
modifiedTensor product of vectors via basis decomposition6738ebc1eb8f
| Field | From #3192 | To #3702 |
|---|
| note | `Basis.tensorProduct_apply` describes how `v ⊗ w` expands in the product basis. | `Module.Basis.tensorProduct_apply` describes how `v ⊗ w` expands in the product basis. |
modifiedSymmetric group action on tensor powers341df49d2c93
| Field | From #3192 | To #3702 |
|---|
| mathlib.module | Mathlib.LinearAlgebra.PiTensorProduct | Mathlib.LinearAlgebra.PiTensorProduct.Basic |
modifiedType (r,s) tensora845d2dcb2ee
| Field | From #3192 | To #3702 |
|---|
| mathlib.module | Mathlib.LinearAlgebra.PiTensorProduct | Mathlib.LinearAlgebra.PiTensorProduct.Basic |
modifiedHigher Tor functors and derived tensor producte76a737eecea
| Field | From #3192 | To #3702 |
|---|
| mathlib.decl | Tor | CategoryTheory.Tor |
| note | Mathlib defines `Tor n : C ⥤ C ⥤ C` in `CategoryTheory.Monoidal.Tor`; a single packaged 'derived tensor product' term is not standard. | Mathlib defines `CategoryTheory.Tor n : C ⥤ C ⥤ C` in `CategoryTheory.Monoidal.Tor`; a single packaged 'derived tensor product' term is not standard. |
addedMonoidal category as general setting for tensor producta8dcb09d0015
addedTensor product of graphs (categorical product)6b671c2373a8
addedKronecker product of matricesaa7f4b3e390e
addedTensor product distributes over direct sums (graded tensor product)99a5e9ec16b2
addedFree module on a set (Cartesian product basis for L)00ce1c474f36