Commit 2023-06-02 11:07 fa72225a

View on Github →

feat: port NumberTheory.Liouville.Basic (#4576)

Estimated changes

Modified Mathlib.lean

Created Mathlib/NumberTheory/Liouville/Basic.lean

added theorem Liouville.exists_one_le_pow_mul_dist

added theorem Liouville.exists_pos_real_of_irrational_root

added def Liouville