Commit 2023-06-02 20:28 171df1ee

View on Github →

feat: port NumberTheory.Liouville.LiouvilleWith (#4596)

Estimated changes

Modified Mathlib.lean

Created Mathlib/NumberTheory/Liouville/LiouvilleWith.lean

added theorem Liouville.frequently_exists_num

added theorem LiouvilleWith.add_int

added theorem LiouvilleWith.add_int_iff

added theorem LiouvilleWith.add_nat

added theorem LiouvilleWith.add_nat_iff

added theorem LiouvilleWith.add_rat

added theorem LiouvilleWith.add_rat_iff

added theorem LiouvilleWith.exists_pos

added theorem LiouvilleWith.frequently_lt_rpow_neg

added theorem LiouvilleWith.int_add

added theorem LiouvilleWith.int_add_iff

added theorem LiouvilleWith.int_mul

added theorem LiouvilleWith.int_mul_iff

added theorem LiouvilleWith.int_sub

added theorem LiouvilleWith.int_sub_iff

added theorem LiouvilleWith.mono

added theorem LiouvilleWith.mul_int

added theorem LiouvilleWith.mul_int_iff

added theorem LiouvilleWith.mul_nat

added theorem LiouvilleWith.mul_nat_iff

added theorem LiouvilleWith.mul_rat

added theorem LiouvilleWith.mul_rat_iff

added theorem LiouvilleWith.nat_add

added theorem LiouvilleWith.nat_add_iff

added theorem LiouvilleWith.nat_mul

added theorem LiouvilleWith.nat_mul_iff

added theorem LiouvilleWith.nat_sub

added theorem LiouvilleWith.nat_sub_iff

added theorem LiouvilleWith.ne_cast_int

added theorem LiouvilleWith.neg_iff

added theorem LiouvilleWith.rat_add

added theorem LiouvilleWith.rat_add_iff

added theorem LiouvilleWith.rat_mul

added theorem LiouvilleWith.rat_mul_iff

added theorem LiouvilleWith.rat_sub

added theorem LiouvilleWith.rat_sub_iff

added theorem LiouvilleWith.sub_int

added theorem LiouvilleWith.sub_int_iff

added theorem LiouvilleWith.sub_nat

added theorem LiouvilleWith.sub_nat_iff

added theorem LiouvilleWith.sub_rat

added theorem LiouvilleWith.sub_rat_iff

added def LiouvilleWith

added theorem forall_liouvilleWith_iff

added theorem liouvilleWith_one