feat: port Algebra.Algebra.Subalgebra.Basic (#2743)

Co-authored-by: ChrisHughes24 <chrishughes24@gmail.com>
leanprover-community · Mar 10, 2023 · da1f9e0 · da1f9e0
1 parent a423cad
commit da1f9e0
Show file tree

Hide file tree

Showing 3 changed files with 1,516 additions and 6 deletions.
diff --git a/Mathlib.lean b/Mathlib.lean
@@ -8,6 +8,7 @@ import Mathlib.Algebra.Algebra.Operations
 import Mathlib.Algebra.Algebra.Pi
 import Mathlib.Algebra.Algebra.Prod
 import Mathlib.Algebra.Algebra.RestrictScalars
+import Mathlib.Algebra.Algebra.Subalgebra.Basic
 import Mathlib.Algebra.Algebra.Tower
 import Mathlib.Algebra.Associated
 import Mathlib.Algebra.BigOperators.Associated