Commit 2023-06-05 05:13 0aab1331

View on Github →

feat: port NumberTheory.Liouville.Measure (#4613)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/MeasureTheory/Measure/Haar/OfBasis.lean

Created Mathlib/NumberTheory/Liouville/Measure.lean

added theorem Real.disjoint_residual_ae

added theorem ae_not_liouville

added theorem ae_not_liouvilleWith

added theorem setOf_liouvilleWith_subset_aux

added theorem volume_iUnion_setOf_liouvilleWith

added theorem volume_setOf_liouville