feat: port Algebra.Category.Mon.Basic (#2902)

Co-authored-by: Joël Riou <joel.riou@universite-paris-saclay.fr>

Author: mo271

Mathlib.lean

@@ -29,6 +29,7 @@ import Mathlib.Algebra.BigOperators.Pi
 import Mathlib.Algebra.BigOperators.Ring
 import Mathlib.Algebra.BigOperators.RingEquiv
 import Mathlib.Algebra.Bounds
+import Mathlib.Algebra.Category.MonCat.Basic
 import Mathlib.Algebra.CharP.Basic
 import Mathlib.Algebra.CharP.ExpChar
 import Mathlib.Algebra.CharP.Invertible