Commit 2023-06-02 16:32 55a106e9

View on Github →

feat: port NumberTheory.Liouville.Residual (#4592)

Estimated changes

Modified Mathlib.lean

Created Mathlib/NumberTheory/Liouville/Residual.lean

added theorem dense_liouville

added theorem eventually_residual_liouville

added theorem isGδ_setOf_liouville

added theorem setOf_liouville_eq_iInter_iUnion

added theorem setOf_liouville_eq_irrational_inter_iInter_iUnion