Commit 2024-02-06 09:06 34bbb84e

View on Github →

chore(Analysis/BoxIntegral): Fintype -> Finite (#10292)

Estimated changes

Modified Mathlib/Analysis/BoxIntegral/Partition/Additive.lean

modified def BoxIntegral.BoxAdditiveMap.ofMapSplitAdd

Modified Mathlib/Analysis/BoxIntegral/Partition/Measure.lean

modified def MeasureTheory.Measure.toBoxAdditive

Modified Mathlib/Analysis/BoxIntegral/Partition/Split.lean