Def continuous_linear_map.comp_Lp

Modification history

2021-07-11 20:13

src/measure_theory/lp_space.lean

feat(measure_theory/{lp_space,set_integral}): extend linear map lemmas from R to is_R_or_C (#8210)

Modified continuous_linear_map.comp_Lp View on Github →

2021-02-10 00:03

src/measure_theory/lp_space.lean

feat(measure_theory/lp_space): add more API on Lp spaces (#6042) …

Added continuous_linear_map.comp_Lp View on Github →