feat: port Algebra.Algebra.Equiv (#2413)

Co-authored-by: qawbecrdtey <qawbecrdtey@naver.com> Co-authored-by: Lukas Miaskiwskyi <lukas.mias@gmail.com> Co-authored-by: Anne Baanen <t.baanen@vu.nl>
leanprover-community · Feb 28, 2023 · 972a45b · 972a45b
1 parent 39c00cb
commit 972a45b
Show file tree

Hide file tree

Showing 2 changed files with 817 additions and 0 deletions.
diff --git a/Mathlib.lean b/Mathlib.lean
@@ -1,6 +1,7 @@
 import Mathlib.Algebra.Abs
 import Mathlib.Algebra.AddTorsor
 import Mathlib.Algebra.Algebra.Basic
+import Mathlib.Algebra.Algebra.Equiv
 import Mathlib.Algebra.Algebra.Hom
 import Mathlib.Algebra.Algebra.Prod
 import Mathlib.Algebra.Associated