basic): `div_neg_self`, `neg_div_self` (#11438)

Commit

4 years ago

feat(algebra/field/basic): `div_neg_self`, `neg_div_self` (#11438) I think these two lemmas are useful as `simp` lemmas, but they don't seem to be there already.

Author

jsm28

Parents

201aeaa3

mathlib 22a9f2eb - feat(algebra/field/basic): `div_neg_self`, `neg_div_self` (#11438)

mathlib
22a9f2eb - feat(algebra/field/basic): `div_neg_self`, `neg_div_self` (#11438)