Commit 2024-07-18 21:00 03960f7f

feat(CstarRing): various lemmas related to the spectral order and the CFC (#13676) This PR proves various lemmas for C*-algebras, such as

• if a ≤ b, then ‖a‖ ≤ ‖b‖
• star a * b *a ≤ ‖b‖ • (star a * a)
• if a is positive, then ‖a‖ ∈ spectrum ℝ a. It also puts an order instance on Unitization ℂ A, needed to prove the above.
• depends on: #13650
• depends on: #13673