Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-09-07 19:41 c7d6a8e7

View on Github →

feat(ring_theory/unique_factorization_domain): descending chain condition for divisibility (#4031) Defines the strict divisibility relation dvd_not_unit Defines class wf_dvd_monoid, indicating that dvd_not_unit is well-founded Provides instances of wf_dvd_monoid Prepares to refactor unique_factorization_domain as a predicate extending wf_dvd_monoid

Estimated changes

Modified src/algebra/associated.lean

added theorem associates.dvd_not_unit_iff_lt

added theorem associates.dvd_not_unit_of_lt

added theorem associates.irreducible_mk

deleted theorem associates.irreducible_mk_iff

deleted theorem associates.le_of_mul_le_mul_right

added theorem associates.mk_dvd_not_unit_mk_iff

added theorem associates.mk_surjective

Modified src/algebra/divisibility.lean

added def dvd_not_unit

added theorem dvd_not_unit_of_dvd_of_not_dvd

Modified src/field_theory/splitting_field.lean

Modified src/ring_theory/ideal/basic.lean

Modified src/ring_theory/noetherian.lean

deleted theorem is_noetherian_ring.exists_factors

deleted theorem is_noetherian_ring.exists_irreducible_factor

deleted theorem is_noetherian_ring.irreducible_induction_on

deleted theorem is_noetherian_ring.well_founded_dvd_not_unit

Modified src/ring_theory/polynomial/basic.lean

Modified src/ring_theory/principal_ideal_domain.lean

Modified src/ring_theory/unique_factorization_domain.lean

added theorem wf_dvd_monoid.exists_factors

added theorem wf_dvd_monoid.exists_irreducible_factor

added theorem wf_dvd_monoid.iff_well_founded_associates

added theorem wf_dvd_monoid.induction_on_irreducible

added theorem wf_dvd_monoid.of_well_founded_associates

added theorem wf_dvd_monoid.of_wf_dvd_monoid_associates

added theorem wf_dvd_monoid.well_founded_associates