Revision #1621 → #2659 · back to history
modifiedTensor product from bases40ebd6614177
| Field | From #1621 | To #2659 |
|---|
| mathlib.decl | Basis.tensorProduct | Module.Basis.tensorProduct |
| provenance | ai | ai-moderated |
modifiedTensor product of vectors via basis decomposition6738ebc1eb8f
| Field | From #1621 | To #2659 |
|---|
| mathlib.decl | Basis.tensorProduct_apply | Module.Basis.tensorProduct_apply |
| provenance | ai | ai-moderated |
modifiedTensor product is a bifunctor1277693e53ef
| Field | From #1621 | To #2659 |
|---|
| mathlib.decl | ModuleCat.instMonoidalCategory | ModuleCat.monoidalCategory |
| provenance | ai | ai-moderated |
modifiedAdjoint representation via tensor productd48cdc7552a2
| Field | From #1621 | To #2659 |
|---|
| mathlib.decl | LieModule.instTensorProduct | TensorProduct.LieModule.lieModule |
| provenance | ai | ai-moderated |
modifiedTensor product of representations / algebrasfbd94a175ce9
| Field | From #1621 | To #2659 |
|---|
| mathlib.decl | Rep.tensor | Representation.tprod |
| provenance | ai | ai-moderated |