Skip to content
This repository was archived by the owner on Jul 24, 2024. It is now read-only.

Commit 011cafb

Browse files
loefflerdsgouezel
loefflerd
and
sgouezel
committed
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>
1 parent 86d0406 commit 011cafb

6 files changed

Lines changed: 1493 additions & 1462 deletions

File tree

‎archive/100-theorems-list/9_area_of_a_circle.lean‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -3,7 +3,7 @@ Copyright (c) 2021 James Arthur, Benjamin Davidson, Andrew Souther. All rights r
33
Released under Apache 2.0 license as described in the file LICENSE.
44
Authors: James Arthur, Benjamin Davidson, Andrew Souther
55
-/
6-
import measure_theory.integral.interval_integral
6+
import measure_theory.integral.fund_thm_calculus
77
import analysis.special_functions.sqrt
88
import analysis.special_functions.trigonometric.inverse_deriv
99

‎src/analysis/fourier/add_circle.lean‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -11,6 +11,7 @@ import measure_theory.function.l2_space
1111
import measure_theory.group.integration
1212
import measure_theory.integral.periodic
1313
import topology.continuous_function.stone_weierstrass
14+
import measure_theory.integral.fund_thm_calculus
1415

1516
/-!
1617

‎src/analysis/special_functions/integrals.lean‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -3,7 +3,7 @@ Copyright (c) 2021 Benjamin Davidson. All rights reserved.
33
Released under Apache 2.0 license as described in the file LICENSE.
44
Authors: Benjamin Davidson
55
-/
6-
import measure_theory.integral.interval_integral
6+
import measure_theory.integral.fund_thm_calculus
77
import analysis.special_functions.trigonometric.arctan_deriv
88

99
/-!

0 commit comments

Comments
 (0)