Commit 2024-05-29 01:19 1024fc50
View on Github →feat: a self-adjoint element of a C*-algebra is upper bounded by the algebra map of its norm (#13296)
This PR shows that a ≤ algebraMap ℝ A ‖a‖ for a self-adjoint element a : A of a C*-algebra.
feat: a self-adjoint element of a C*-algebra is upper bounded by the algebra map of its norm (#13296)
This PR shows that a ≤ algebraMap ℝ A ‖a‖ for a self-adjoint element a : A of a C*-algebra.