feat: port Algebra.MonoidAlgebra.Basic (#2589)

leanprover-community · Mar 8, 2023 · db9d23f · db9d23f
1 parent 1a9e5d6
commit db9d23f
Show file tree

Hide file tree

Showing 2 changed files with 2,048 additions and 0 deletions.
diff --git a/Mathlib.lean b/Mathlib.lean
@@ -123,6 +123,7 @@ import Mathlib.Algebra.Module.Submodule.Bilinear
 import Mathlib.Algebra.Module.Submodule.Lattice
 import Mathlib.Algebra.Module.Submodule.Pointwise
 import Mathlib.Algebra.Module.ULift
+import Mathlib.Algebra.MonoidAlgebra.Basic
 import Mathlib.Algebra.NeZero
 import Mathlib.Algebra.Opposites
 import Mathlib.Algebra.Order.AbsoluteValue