mathlib3

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

feat(measure_theory/{lp_space,set_integral}): extend linear map lemmas from R to is_R_or_C (#8210) Co-authored-by: Rémy Degenne <remydegenne@gmail.com> Co-authored-by: RemyDegenne <remydegenne@gmail.com>