Commit 2022-12-14 08:19 d261339c

View on Github →

feat port data.int.least_greatest (#1003) Port of data.int.least_greatest based on 3342d1b2178381196f818146ff79bc0e7ccd9e2d

Estimated changes

Modified Mathlib.lean

Created Mathlib/Data/Int/LeastGreatest.lean

added theorem Int.coe_greatestOfBdd_eq

added theorem Int.coe_leastOfBdd_eq

added theorem Int.exists_greatest_of_bdd

added theorem Int.exists_least_of_bdd

added def Int.greatestOfBdd

added def Int.leastOfBdd