Mathlib v3 is deprecated. Go to Mathlib v4

Theorem self_adjoint.nnnorm_pow_two_pow

Modification history

2022-02-23 17:43
src/analysis/normed_space/star/basic.lean
feat(analysis/normed_space/star/spectrum): prove the spectral radius of a selfadjoint element in a C*-algebra is its norm. (#12211) …
Added self_adjoint.nnnorm_pow_two_powView on Github →