The monoidal structure on QuadraticModuleCat
is symmetric. #
In this file we show:
QuadraticModuleCat.instSymmetricCategory : SymmetricCategory (QuadraticModuleCat.{u} R)
Implementation notes #
This file essentially mirrors Mathlib/Algebra/Category/AlgCat/Symmetric.lean
.
Equations
- One or more equations did not get rendered due to their size.
forget₂ (QuadraticModuleCat R) (ModuleCat R)
is a braided functor.
Equations
- One or more equations did not get rendered due to their size.