Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-10-25 22:55 34b99336

View on Github →

feat(number_theory/liouville): the set of Liouville numbers has measure zero (#9702) As a corollary, the filters residual ℝ and volume.ae are disjoint.

Estimated changes

added theorem liouville_with.add_int
added theorem liouville_with.add_nat
added theorem liouville_with.add_rat
added theorem liouville_with.int_add
added theorem liouville_with.int_mul
added theorem liouville_with.int_sub
added theorem liouville_with.mono
added theorem liouville_with.mul_int
added theorem liouville_with.mul_nat
added theorem liouville_with.mul_rat
added theorem liouville_with.nat_add
added theorem liouville_with.nat_mul
added theorem liouville_with.nat_sub
added theorem liouville_with.neg_iff
added theorem liouville_with.rat_add
added theorem liouville_with.rat_mul
added theorem liouville_with.rat_sub
added theorem liouville_with.sub_int
added theorem liouville_with.sub_nat
added theorem liouville_with.sub_rat
added def liouville_with
added theorem liouville_with_one
added theorem ae_not_liouville
added theorem ae_not_liouville_with