Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-07-11 20:13 19beb127

View on Github →

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

Estimated changes