chore(algebra/field): deduplicate with group_with_zero (#3015)
For historical reasons there are lots of lemmas we prove for `group_with_zero`, then again for a `division_ring`. Merge some of them.
Co-authored-by: Bryan Gin-ge Chen <bryangingechen@gmail.com>
