Theorem IsSelfAdjoint.norm_mul_self

Modification history

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