Commit 2026-02-25 17:28 e580ff89
View on Github →feat: add a LE version of previous lt_one_iff_num_lt_denom theorem (#35097) The following is more useful due to the partial order application of LE in comparison to LT.
feat: add a LE version of previous lt_one_iff_num_lt_denom theorem (#35097) The following is more useful due to the partial order application of LE in comparison to LT.