Commit 2026-03-26 17:12 6731166f
View on Github →chore: drop div_lt_div_* theorem version for integers (#36876) More general theorems like div_lt_div_iff₀ already exist and this theorem specialized for integer-to-rational casts is both unused in mathlib and its removal will decrease future maintenance burden.