feat: define NonUnitalSubalgebra and develop basic API (#5512)

This continues the non-unital-ization of mathlib. - [x] depends on: #5151
leanprover-community · Aug 14, 2023 · 9d30220 · 9d30220
1 parent c059129
commit 9d30220
Show file tree

Hide file tree

Showing 6 changed files with 1,098 additions and 1 deletion.
diff --git a/Mathlib.lean b/Mathlib.lean
@@ -4,6 +4,7 @@ import Mathlib.Algebra.Algebra.Basic
 import Mathlib.Algebra.Algebra.Bilinear
 import Mathlib.Algebra.Algebra.Equiv
 import Mathlib.Algebra.Algebra.Hom
+import Mathlib.Algebra.Algebra.NonUnitalSubalgebra
 import Mathlib.Algebra.Algebra.Operations
 import Mathlib.Algebra.Algebra.Pi
 import Mathlib.Algebra.Algebra.Prod