Commit 2026-05-05 19:39 be685cbb

View on Github →

chore(CategoryTheory/Monoidal): additivize ModObj (#38722)

Estimated changes

Modified Mathlib/CategoryTheory/Monoidal/Mod.lean

added structure CategoryTheory.AddMod.Hom

added structure CategoryTheory.AddMod

modified theorem CategoryTheory.ModObj.smul_eq_mul

Modified Mathlib/Tactic/Translate/ToAdditive.lean