Theorem OrthonormalBasis.norm_le_card_mul_iSup_norm_inner

Modification history

2025-04-07 13:30
Mathlib/Analysis/InnerProductSpace/PiL2.lean
feat(MeasureTheory): tightness criterion in finite dimensional inner product spaces (#23534) …
Added OrthonormalBasis.norm_le_card_mul_iSup_norm_innerView on Github →