Def QuadraticModuleCat.toModuleCatMonoidalFunctor

Modification history

2023-10-25 10:47

Mathlib/LinearAlgebra/QuadraticForm/QuadraticModuleCat/Monoidal.lean

refactor: Move the data fields of `MonoidalCategory` into a `Struct` class (#7279) …

Modified QuadraticModuleCat.toModuleCatMonoidalFunctor View on Github →

2023-10-17 07:52

Mathlib/LinearAlgebra/QuadraticForm/QuadraticModuleCat/Monoidal.lean

feat: MonoidalCategory (QuadraticModuleCat R) (#7244) …

Added QuadraticModuleCat.toModuleCatMonoidalFunctor View on Github →