Commit 2025-07-12 22:24 1ceeead5

View on Github →

feat(CategoryTheory/Monoidal/Mod): γ[M, M] = μ[M] (#27046) From Toric

Estimated changes

added theorem Mod_Class.smul_eq_mul