Skip to content

feat(Analysis/CStarAlgebra/Extreme): a C⋆-algebra is unital iff there exists an extreme point in the closed unit ball#36327

Open
themathqueen wants to merge 29 commits into
leanprover-community:masterfrom
themathqueen:extreme_unital
Open

feat(Analysis/CStarAlgebra/Extreme): a C⋆-algebra is unital iff there exists an extreme point in the closed unit ball#36327
themathqueen wants to merge 29 commits into
leanprover-community:masterfrom
themathqueen:extreme_unital

cleanup

5569c7c
Select commit
Loading
Failed to load commit list.
Sign in for the full log view