Commit 2024-04-16 07:44 8fa5a3ae

View on Github →

chore: tidy various files (#12121)

Estimated changes

Modified Mathlib/Algebra/Function/Indicator.lean

Modified Mathlib/Data/Nat/ChineseRemainder.lean

Modified Mathlib/MeasureTheory/Integral/Lebesgue.lean

modified theorem MeasureTheory.lintegral_dirac'

modified theorem MeasureTheory.lintegral_mul_const_le

modified theorem MeasureTheory.lintegral_smul_measure

Modified Mathlib/NumberTheory/BernoulliPolynomials.lean

Modified Mathlib/Order/Hom/CompleteLattice.lean

Modified Mathlib/Order/SupClosed.lean

modified theorem IsLowerSet.infClosed