feat: port Algebra.Module.Basic (#1169)

One question (now resolved) posted at https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/Heterogeneous.20scalar.20multiplication Co-authored-by: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com> Co-authored-by: Frédéric Dupuis <dupuisf@iro.umontreal.ca> Co-authored-by: Frédéric Dupuis <31101893+dupuisf@users.noreply.github.com>
leanprover-community · Dec 31, 2022 · 4c1cc66 · 4c1cc66
1 parent f5db9bf
commit 4c1cc66
Show file tree

Hide file tree

Showing 2 changed files with 778 additions and 0 deletions.
diff --git a/Mathlib.lean b/Mathlib.lean
@@ -58,6 +58,7 @@ import Mathlib.Algebra.Hom.Ring
 import Mathlib.Algebra.Hom.Units
 import Mathlib.Algebra.Homology.ComplexShape
 import Mathlib.Algebra.Invertible
+import Mathlib.Algebra.Module.Basic
 import Mathlib.Algebra.NeZero
 import Mathlib.Algebra.Opposites
 import Mathlib.Algebra.Order.AbsoluteValue