feat : port Algebra.Module.Equiv (#1732)

leanprover-community · Jan 27, 2023 · 0298ff3 · 0298ff3
1 parent ace49f1
commit 0298ff3
Show file tree

Hide file tree

Showing 2 changed files with 861 additions and 0 deletions.
diff --git a/Mathlib.lean b/Mathlib.lean
@@ -85,6 +85,7 @@ import Mathlib.Algebra.IndicatorFunction
 import Mathlib.Algebra.Invertible
 import Mathlib.Algebra.Module.Basic
 import Mathlib.Algebra.Module.BigOperators
+import Mathlib.Algebra.Module.Equiv
 import Mathlib.Algebra.Module.Hom
 import Mathlib.Algebra.Module.LinearMap
 import Mathlib.Algebra.Module.Pi