mathlib icon indicating copy to clipboard operation
mathlib copied to clipboard

Published 20 hours ago • verified publisher icon leanprover-community

feat(algebra/star/subalgebra): develop some API for `star_subalgebra`

Open j-loreaux opened this issue 3 years ago • 0 comments

Some of this is necessary to define the (closed) C⋆-algebra generated by a single element, which is in turn necessary to define the continuous functional calculus.

Open in Gitpod

j-loreaux avatar Oct 10 '22 23:10 j-loreaux