Theorem neg_div'

Modification history

2025-10-22 23:09
Mathlib/Algebra/Ring/Basic.lean
feat(Algebra/Ring/Basic): add `a / -b = -a / b` (#30261)
Modified neg_div'View on Github →
2025-01-07 20:33
Mathlib/Algebra/Field/Basic.lean
chore: move results about `DivisionMonoid` + `HasDistribNeg` (#20551) …
Modified neg_div'View on Github →
2022-12-14 09:49
Mathlib/Algebra/Field/Basic.lean
feat port Algebra.Field.Basic (#975) …
Added neg_div'View on Github →