Theorem div_le_div₀

Modification history

2024-11-19 19:36

Mathlib/Algebra/Order/GroupWithZero/Unbundled.lean

chore: generalise `div_le_div` to groups with zero (#18917) …

Modified div_le_div₀ View on Github →

2024-08-26 13:45

Mathlib/Algebra/Order/GroupWithZero/Canonical.lean

refactor: Generalise ordered field lemmas to ordered groups with zero (#16036) …

Modified div_le_div₀ View on Github →

2024-05-31 00:19

Mathlib/Algebra/Order/GroupWithZero/Canonical.lean

chore: fix formatting of many misplaced "by"s (#13204)

Modified div_le_div₀ View on Github →

2022-12-12 09:20

Mathlib/Algebra/Order/WithZero.lean

feat: port Algebra.Order.WithZero (#903) …

Added div_le_div₀ View on Github →