Commit 2023-06-19 10:10 129e53be

View on Github →

feat: port NumberTheory.WellApproximable (#5255)

Estimated changes

Modified Mathlib.lean

Created Mathlib/NumberTheory/WellApproximable.lean

added theorem AddCircle.addWellApproximable_ae_empty_or_univ

added theorem UnitAddCircle.mem_addWellApproximable_iff

added theorem UnitAddCircle.mem_approxAddOrderOf_iff

added theorem approxOrderOf.image_pow_subset

added theorem approxOrderOf.image_pow_subset_of_coprime

added theorem approxOrderOf.smul_eq_of_mul_dvd

added theorem approxOrderOf.smul_subset_of_coprime

added def approxOrderOf

added theorem mem_approxOrderOf_iff

added theorem mem_wellApproximable_iff

added def wellApproximable