Commit 2025-10-29 04:59 4c8d3005

feat(Algebra/Category): symmetric monoidal structure on SemimoduleCat (#30638)

• Construct the symmetric monoidal structure on SemimoduleCat, and transport it to the same structure on ModuleCat (in a way preserving pre-existing defeqs) using the equivalence ModuleCat.equivalenceSemimoduleCat between the categories. Just a few proofs in the Representation library need to be fixed (in a straightforward way). Public API for ModuleCat is duplicated to SemimoduleCat.