Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-10-19 09:31 ff3e868c

View on Github →

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.

Estimated changes