Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2018-10-18 09:43 f2beca80

View on Github →

feat(ring_theory): prove principal_ideal_domain is unique factorization domain

Estimated changes

Modified linear_algebra/submodule.lean

added theorem submodule.mem_span_singleton

added theorem submodule.span_singleton_subset

Modified ring_theory/associated.lean

deleted theorem associated.associated_of_dvd_dvd

deleted theorem associated.associated_one_iff_is_unit

deleted theorem associated.associated_one_of_associated_mul_one

deleted theorem associated.associated_one_of_mul_eq_one

deleted theorem associated.associated_zero_iff_eq_zero

deleted theorem associated.unit_associated_one

added theorem associated_mul_mul

added theorem associated_of_dvd_dvd

added theorem associated_one_iff_is_unit

added theorem associated_one_of_associated_mul_one

added theorem associated_one_of_mul_eq_one

added theorem associated_zero_iff_eq_zero

added theorem associates.dvd_eq_le

added theorem associates.eq_of_mul_eq_mul_left

added theorem associates.exists_mem_multiset_le_of_prime

added theorem associates.le_of_mul_le_mul_left

added theorem associates.one_or_eq_of_le_of_prime

added def associates.prime

added theorem associates.prime_mk

added theorem exists_mem_multiset_dvd_of_prime

modified theorem is_unit_iff_dvd_one

modified theorem is_unit_iff_forall_dvd

deleted theorem is_unit_mul_units

added theorem is_unit_of_dvd_one

added theorem is_unit_of_mul_one

added theorem not_prime_zero

added def prime

added theorem unit_associated_one

added theorem units.is_unit_mul_units

deleted theorem units.is_unit_of_mul_one

Modified ring_theory/principal_ideal_domain.lean

modified theorem is_prime_ideal.to_maximal_ideal

modified theorem mod_mem_iff

added theorem principal_ideal_domain.associated_of_associated_prod_prod

added theorem principal_ideal_domain.associates_prime_of_irreducible

added theorem principal_ideal_domain.eq_of_prod_eq_associates

added theorem principal_ideal_domain.exists_factors

added theorem principal_ideal_domain.factors_decreasing

added theorem principal_ideal_domain.factors_spec

added theorem principal_ideal_domain.is_maximal_ideal_of_irreducible

added theorem principal_ideal_domain.is_noetherian_ring

added theorem principal_ideal_domain.prime_of_irreducible