Theorem IsBoundedSMul.of_enorm_smul_le

Modification history

2025-05-12 15:41
Mathlib/Analysis/Normed/MulAction.lean
refactor(LpSeminorm/Basic, LpSpace/Basic): generalise more lemmas to enorms (#24640) …
Added IsBoundedSMul.of_enorm_smul_leView on Github →