Commit 2024-09-12 16:24 862c6652

View on Github →

chore: namespace lemmas to CStarAlgebra instead of CStarRing (#16653) This changes the namespace from CStarRing to CStarAlgebra for any lemmas whose hypotheses imply Module ℂ A. We reserve CStarRing for lemmas pertaining only to the normed ring structure, but which do not involve the -algebra structure.

Estimated changes

deleted theorem CStarRing.inv_le_iff
deleted theorem CStarRing.inv_le_one
deleted theorem CStarRing.isClosed_nonneg
deleted theorem CStarRing.isUnit_of_le
deleted theorem CStarRing.le_inv_iff