mathlib3

ff3e868c - refactor(algebra/domain): make domain and integral_domain mixins (#9719)

refactor(algebra/domain): make domain and integral_domain mixins (#9719) This PR turns `domain` and `integral_domain` into mixins. There's quite a lot of work here, as the unused argument linter then forces us to do some generalizations! (i.e. getting rid of unnecessary `integral_domain` arguments). This PR does the minimum possible generalization: #9739 does some more. In a subsequent PR we can unify `domain` and `integral_domain`, which now only differ in their typeclass requirements. This also remove use of `old_structure_cmd` in `euclidean_domain`. - [x] depends on: #9725 [An RFC] - [x] depends on: #9736 [](https://gitpod.io/from-referrer/) Co-authored-by: Scott Morrison <scott.morrison@gmail.com>