Skip to content

Commit c24d329

Browse files
committed
feat: port Algebra.Star.Subalgebra (#2819)
Note: Lean was continually crashing on me as I was porting this file, I believe sure to autoparams. - [x] depends on: #2817
1 parent e5b2bcd commit c24d329

File tree

2 files changed

+794
-0
lines changed

2 files changed

+794
-0
lines changed

Mathlib.lean

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -237,6 +237,7 @@ import Mathlib.Algebra.Star.Pointwise
237237
import Mathlib.Algebra.Star.Prod
238238
import Mathlib.Algebra.Star.SelfAdjoint
239239
import Mathlib.Algebra.Star.StarAlgHom
240+
import Mathlib.Algebra.Star.Subalgebra
240241
import Mathlib.Algebra.Star.Unitary
241242
import Mathlib.Algebra.Support
242243
import Mathlib.Algebra.Tropical.Basic

0 commit comments

Comments
 (0)