Theorem div_eq_div_of_div_eq_div

Modification history

2025-07-07 17:19
Mathlib/Algebra/GroupWithZero/Units/Basic.lean
feat(Algebra): `a / n ≤ a` if `n : ℕ` and `0 ≤ a` (#26658) …
Added div_eq_div_of_div_eq_divView on Github →