mathlib3

feced767 - feat(algebra/*): Noncomputable `group` structures from `is_unit` (#5427)

feat(algebra/*): Noncomputable `group` structures from `is_unit` (#5427) Noncomputably defines the following group structures given that all (nonzero) elements are units: - `monoid` -> `group` - `comm_monoid` -> `comm_group` - `monoid_with_zero` -> `comm_group_with_zero` - `comm_monoid_with_zero` -> `comm_group_with_zero` - `ring` -> `division_ring` - `comm_ring` -> `field` Co-authored-by: Aaron Anderson <65780815+awainverse@users.noreply.github.com>