Commit 2023-04-30 06:51 011cafb4
View on Github →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.