feat(NumberTheory/Transcendental/Liouville): irrational reals are LiouvilleWith for 1 < p ≤ 2 - #43595

feat(NumberTheory/Transcendental/Liouville): irrational reals are LiouvilleWith for 1 < p ≤ 2#43595

localecho wants to merge 2 commits into

leanprover-community:masterleanprover-community/mathlib4:masterfrom

localecho:liouville-with-gaplocalecho/mathlib4:liouville-with-gapCopy head branch name to clipboard