Mathlib Changelog
v3
Changelog
About
Github
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
archive/imo/imo1962_q4.lean
modified
theorem
formula
Modified
src/algebra/algebra/basic.lean
modified
theorem
no_zero_smul_divisors.iff_algebra_map_injective
Modified
src/algebra/algebra/bilinear.lean
Modified
src/algebra/algebra/subalgebra.lean
Modified
src/algebra/char_p/algebra.lean
Modified
src/algebra/euclidean_domain.lean
Modified
src/algebra/field.lean
Modified
src/algebra/gcd_monoid/basic.lean
Modified
src/algebra/gcd_monoid/finset.lean
Modified
src/algebra/group_power/basic.lean
modified
theorem
eq_or_eq_neg_of_sq_eq_sq
Modified
src/algebra/opposites.lean
Modified
src/algebra/order/ring.lean
Modified
src/algebra/quadratic_discriminant.lean
Modified
src/algebra/quaternion.lean
Modified
src/algebra/ring/basic.lean
deleted
theorem
integral_domain.to_is_integral_domain
deleted
theorem
is_integral_domain.to_integral_domain
deleted
structure
is_integral_domain
Modified
src/data/equiv/ring.lean
Modified
src/data/equiv/transfer_instance.lean
Modified
src/data/mv_polynomial/funext.lean
Modified
src/data/mv_polynomial/variables.lean
Modified
src/data/polynomial/cancel_leads.lean
modified
theorem
polynomial.nat_degree_cancel_leads_lt_of_nat_degree_le_nat_degree
Modified
src/data/polynomial/derivative.lean
Modified
src/data/polynomial/field_division.lean
Modified
src/data/polynomial/integral_normalization.lean
Modified
src/data/polynomial/mirror.lean
modified
theorem
polynomial.irreducible_of_mirror
modified
theorem
polynomial.mirror_mul_of_domain
modified
theorem
polynomial.mirror_smul
Modified
src/data/polynomial/reverse.lean
modified
theorem
polynomial.reverse_mul_of_domain
modified
theorem
polynomial.trailing_coeff_mul
Modified
src/data/polynomial/ring_division.lean
deleted
theorem
is_integral_domain.polynomial
modified
theorem
polynomial.eq_of_infinite_eval_eq
modified
theorem
polynomial.leading_coeff_div_by_monic_of_monic
modified
def
polynomial.nth_roots_finset
modified
def
polynomial.root_set
modified
theorem
polynomial.root_set_C
modified
theorem
polynomial.root_set_def
modified
theorem
polynomial.root_set_zero
Modified
src/data/rat/basic.lean
Modified
src/data/real/basic.lean
Modified
src/data/real/cau_seq.lean
Modified
src/data/zmod/basic.lean
Modified
src/field_theory/finite/basic.lean
modified
theorem
char_p.sq_add_sq
Modified
src/field_theory/fixed.lean
Modified
src/field_theory/is_alg_closed/basic.lean
modified
theorem
is_alg_closed.algebra_map_surjective_of_is_algebraic
modified
theorem
is_alg_closed.algebra_map_surjective_of_is_integral
Modified
src/field_theory/minpoly.lean
modified
theorem
minpoly.gcd_domain_eq_field_fractions
Modified
src/field_theory/perfect_closure.lean
modified
theorem
perfect_closure.eq_iff
Modified
src/field_theory/separable.lean
Modified
src/linear_algebra/bilinear_form.lean
Modified
src/linear_algebra/determinant.lean
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
def
matrix.index_equiv_of_inv
Modified
src/linear_algebra/finite_dimensional.lean
Modified
src/linear_algebra/free_module/pid.lean
modified
theorem
ideal.rank_eq
Modified
src/linear_algebra/matrix/nonsingular_inverse.lean
Modified
src/linear_algebra/matrix/to_linear_equiv.lean
modified
theorem
matrix.exists_mul_vec_eq_zero_iff
modified
theorem
matrix.exists_vec_mul_eq_zero_iff
modified
theorem
matrix.nondegenerate_iff_det_ne_zero
Modified
src/linear_algebra/sesquilinear_form.lean
Modified
src/number_theory/class_number/finite.lean
Modified
src/number_theory/function_field.lean
Modified
src/number_theory/padics/padic_integers.lean
Modified
src/number_theory/zsqrtd/basic.lean
Modified
src/ring_theory/adjoin_root.lean
Modified
src/ring_theory/algebraic.lean
Modified
src/ring_theory/class_group.lean
Modified
src/ring_theory/dedekind_domain.lean
modified
theorem
ring.dimension_le_one.integral_closure
modified
theorem
ring.dimension_le_one.is_integral_closure
Modified
src/ring_theory/discrete_valuation_ring.lean
modified
theorem
discrete_valuation_ring.iff_pid_with_one_nonzero_prime
modified
theorem
discrete_valuation_ring.of_has_unit_mul_pow_irreducible_factorization
Modified
src/ring_theory/eisenstein_criterion.lean
Modified
src/ring_theory/fractional_ideal.lean
Modified
src/ring_theory/hahn_series.lean
modified
theorem
hahn_series.order_mul
Modified
src/ring_theory/ideal/basic.lean
modified
theorem
ideal.bot_prime
modified
theorem
ideal.factors_decreasing
added
theorem
ideal.quotient.is_domain_iff_prime
deleted
theorem
ideal.quotient.is_integral_domain_iff_prime
modified
theorem
ideal.span_singleton_eq_span_singleton
modified
theorem
ideal.span_singleton_lt_span_singleton
Modified
src/ring_theory/ideal/operations.lean
modified
theorem
ideal.mul_eq_bot
modified
theorem
ideal.prod_eq_bot
deleted
theorem
ideal.radical_bot_of_integral_domain
added
theorem
ideal.radical_bot_of_is_domain
modified
theorem
ring_hom.ker_is_prime
Modified
src/ring_theory/ideal/over.lean
modified
theorem
ideal.comap_ne_bot_of_algebraic_mem
modified
theorem
ideal.comap_ne_bot_of_integral_mem
modified
theorem
ideal.comap_ne_bot_of_root_mem
modified
theorem
ideal.eq_bot_of_comap_eq_bot
modified
theorem
ideal.exists_ideal_over_maximal_of_is_integral
Modified
src/ring_theory/integral_closure.lean
Modified
src/ring_theory/integral_domain.lean
deleted
def
division_ring_of_domain
added
def
division_ring_of_is_domain
deleted
def
field_of_integral_domain
added
def
field_of_is_domain
deleted
theorem
is_cyclic_of_subgroup_integral_domain
added
theorem
is_cyclic_of_subgroup_is_domain
Modified
src/ring_theory/integrally_closed.lean
Modified
src/ring_theory/jacobson.lean
Modified
src/ring_theory/localization.lean
deleted
theorem
is_fraction_ring.to_integral_domain
deleted
theorem
is_localization.integral_domain_localization
deleted
theorem
is_localization.integral_domain_of_le_non_zero_divisors
added
theorem
is_localization.is_domain_localization
added
theorem
is_localization.is_domain_of_le_non_zero_divisors
Modified
src/ring_theory/multiplicity.lean
Modified
src/ring_theory/noetherian.lean
Modified
src/ring_theory/norm.lean
modified
theorem
algebra.norm_eq_zero_iff_of_basis
modified
theorem
algebra.norm_ne_zero_iff_of_basis
Modified
src/ring_theory/perfection.lean
Modified
src/ring_theory/polynomial/basic.lean
added
theorem
ideal.is_domain_map_C_quotient
deleted
theorem
ideal.is_integral_domain_map_C_quotient
deleted
theorem
mv_polynomial.integral_domain_fintype
added
theorem
mv_polynomial.is_domain_fin
added
theorem
mv_polynomial.is_domain_fin_zero
added
theorem
mv_polynomial.is_domain_fintype
deleted
theorem
mv_polynomial.is_integral_domain_fin
deleted
theorem
mv_polynomial.is_integral_domain_fin_zero
deleted
theorem
mv_polynomial.is_integral_domain_fintype
Modified
src/ring_theory/polynomial/content.lean
Modified
src/ring_theory/polynomial/cyclotomic.lean
modified
def
polynomial.cyclotomic'
modified
theorem
polynomial.roots_of_cyclotomic
Modified
src/ring_theory/polynomial/gauss_lemma.lean
Modified
src/ring_theory/polynomial/rational_root.lean
Modified
src/ring_theory/polynomial/scale_roots.lean
Modified
src/ring_theory/power_basis.lean
Modified
src/ring_theory/power_series/basic.lean
Modified
src/ring_theory/principal_ideal_domain.lean
modified
theorem
is_prime.to_maximal_ideal
Modified
src/ring_theory/roots_of_unity.lean
modified
def
primitive_roots
Modified
src/ring_theory/subring.lean
Modified
src/ring_theory/unique_factorization_domain.lean
Modified
src/ring_theory/valuation/integral.lean