Skip to content

Commit f4c36e3

Browse files
Ruben-VandeVeldeParcly-Taxelint-y1
committed
feat: port Analysis.BoxIntegral.Partition.Basic (#3438)
Co-authored-by: Jeremy Tan Jie Rui <reddeloostw@gmail.com> Co-authored-by: int-y1 <jason_yuen2007@hotmail.com>
1 parent 262e026 commit f4c36e3

File tree

2 files changed

+797
-0
lines changed

2 files changed

+797
-0
lines changed

Mathlib.lean

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -330,6 +330,7 @@ import Mathlib.Analysis.Asymptotics.SuperpolynomialDecay
330330
import Mathlib.Analysis.Asymptotics.Theta
331331
import Mathlib.Analysis.BoxIntegral.Box.Basic
332332
import Mathlib.Analysis.BoxIntegral.Box.SubboxInduction
333+
import Mathlib.Analysis.BoxIntegral.Partition.Basic
333334
import Mathlib.Analysis.Convex.Basic
334335
import Mathlib.Analysis.Convex.Body
335336
import Mathlib.Analysis.Convex.Caratheodory

0 commit comments

Comments
 (0)