mathlib3
3b279c17 - feat(measure_theory/l2_space): generalize inner_indicator_const_Lp_one from R to is_R_or_C (#8602)

Commit

4 years ago

feat(measure_theory/l2_space): generalize inner_indicator_const_Lp_one from R to is_R_or_C (#8602) Co-authored-by: Rémy Degenne <remydegenne@gmail.com>

Author

RemyDegenne

Parents

d1b2a548

mathlib3 3b279c17 - feat(measure_theory/l2_space): generalize inner_indicator_const_Lp_one from R to is_R_or_C (#8602)

mathlib3
3b279c17 - feat(measure_theory/l2_space): generalize inner_indicator_const_Lp_one from R to is_R_or_C (#8602)