mathlib3
baf5306c - chore(measure_theory/function/lp_space): split file

Commit
2 years ago
chore(measure_theory/function/lp_space): split file This file is very long; this splits out 300 lines of self-contained content about indicator functions.
Author
Parents
Loading