mathlib3
3c1ced3b - feat(data/nat/basic): four lemmas on nat and int division (#13991)

Commit
3 years ago
feat(data/nat/basic): four lemmas on nat and int division (#13991) `lt_div_iff_mul_lt (hnd : d ∣ n) : a < n / d ↔ d * a < n` `div_left_inj (hda : d ∣ a) (hdb : d ∣ b) : a / d = b / d ↔ a = b` (for `ℕ` and `ℤ`) `div_lt_div_of_lt_of_dvd (hdb : d ∣ b) (h : a < b) : a / d < b / d`
Parents
Loading