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

Commits

Commits on Mar 2, 2026

Commits on Mar 5, 2026

Commits on Mar 7, 2026

Commits on Mar 10, 2026

Commits on Mar 11, 2026

Commits on Mar 13, 2026

Commits on Mar 20, 2026

Commits on Apr 9, 2026

Commits on Apr 29, 2026

Commits on Jul 19, 2026

Commits on Jul 20, 2026

Commits on Jul 21, 2026