mathlib3
011cafb4 - chore (measure_theory/integral): split interval_integral.lean into two (#18898)

Commit
2 years ago
chore (measure_theory/integral): split interval_integral.lean into two (#18898) This divides `interval_integral.lean` (currently 2800 lines) into two roughly equal chunks -- moving the variants of FTC into a new file `fund_thm_calculus.lean` and leaving definitions and basic lemmas in the original file. Co-authored-by: sgouezel <sebastien.gouezel@univ-rennes1.fr>
Author
Parents
Loading