Theorem IsSelfAdjoint.nnnorm_mul_self

Modification history

2025-10-08 02:50
Mathlib/Analysis/CStarAlgebra/Basic.lean
feat: add lemmata about selfadjoint elements (#30301) …
Added IsSelfAdjoint.nnnorm_mul_selfView on Github →