Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-10-21 08:38 da01792c

View on Github →

refactor(*): remove integral_domain, rename domain to is_domain (#9748)

Estimated changes

modified theorem formula
modified theorem eq_or_eq_neg_of_sq_eq_sq
deleted structure is_integral_domain
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_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 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 is_prime.to_maximal_ideal
modified def primitive_roots