Commit 2023-09-06 20:46 3ebc913e

View on Github →

chore: tidy various files (#6924)

Estimated changes

Modified Mathlib/Analysis/NormedSpace/lpSpace.lean

Modified Mathlib/Data/Set/Intervals/ProjIcc.lean

added theorem Set.IccExtend_apply

deleted theorem Set.iccExtend_apply

Modified Mathlib/Geometry/Manifold/MFDeriv.lean

Modified Mathlib/Logic/Equiv/Array.lean

Modified Mathlib/MeasureTheory/Function/LocallyIntegrable.lean

Modified Mathlib/MeasureTheory/Integral/FundThmCalculus.lean

added theorem intervalIntegral.FTCFilter.finiteAt_inner

deleted theorem intervalIntegral.FTCFilter.finite_at_inner

Modified Mathlib/MeasureTheory/Integral/IntegrableOn.lean

Modified Mathlib/NumberTheory/Padics/PadicVal.lean

Modified Mathlib/Order/WellFoundedSet.lean

Modified Mathlib/RingTheory/DedekindDomain/Ideal.lean