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

modified theorem formula
modified theorem eq_or_eq_neg_of_sq_eq_sq
modified theorem polynomial.mirror_smul
modified def polynomial.root_set
modified theorem polynomial.root_set_C
modified theorem polynomial.root_set_def
modified theorem polynomial.root_set_finite
modified theorem polynomial.root_set_zero
modified theorem char_p.sq_add_sq
modified theorem perfect_closure.eq_iff
modified def equiv_of_pi_lequiv_pi
modified theorem linear_equiv.is_unit_det'
modified theorem matrix.det_comm'
modified theorem matrix.det_conj
modified theorem ideal.rank_eq
modified theorem mul_generator_self_inv
modified theorem hahn_series.order_mul
modified theorem ideal.bot_prime
modified theorem ideal.factors_decreasing
modified theorem ideal.mul_eq_bot
modified theorem ideal.prod_eq_bot
modified theorem ring_hom.ker_is_prime
modified theorem polynomial.cyclotomic'_one
modified theorem polynomial.cyclotomic'_two
modified theorem polynomial.cyclotomic'_zero
modified theorem is_prime.to_maximal_ideal
modified def primitive_roots