Commit 2024-10-28 14:12 fb0124bc

View on Github →

feat: a / b < 0 → 0 ≤ a → b < 0 (#18260)

Estimated changes

Modified Mathlib/Algebra/Order/GroupWithZero/Unbundled.lean

modified theorem div_nonpos_of_nonneg_of_nonpos

modified theorem inv_neg''

modified theorem inv_nonpos

added theorem neg_of_div_neg_left

added theorem neg_of_div_neg_right