Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-01-10 12:11 f5bf2776

View on Github →

refactor(unique_factorization_domain): simplify definition of UFD

Estimated changes

Modified data/multiset.lean

added theorem multiset.dvd_prod

Modified ring_theory/associated.lean

added theorem associated_mul_left_cancel

added theorem associated_mul_right_cancel

added theorem dvd_iff_dvd_of_rel_left

added theorem dvd_iff_dvd_of_rel_right

added theorem dvd_mul_unit_iff

added theorem eq_zero_iff_of_associated

added theorem exists_associated_mem_of_dvd_prod

added theorem irreducible_iff_of_associated

added theorem irreducible_of_associated

added theorem is_unit_iff_of_associated

added theorem is_unit_unit

added theorem mul_unit_dvd_iff

added theorem ne_zero_iff_of_associated

modified theorem not_prime_zero

added theorem prime_iff_of_associated

added theorem prime_of_associated

added theorem unit_mul_dvd_iff

Modified ring_theory/principal_ideal_domain.lean

Modified ring_theory/unique_factorization_domain.lean

added theorem unique_factorization_domain.factors_irreducible

added theorem unique_factorization_domain.induction_on_prime

added theorem unique_factorization_domain.irreducible_factors

added theorem unique_factorization_domain.irreducible_iff_prime

added def unique_factorization_domain.of_unique_irreducible_factorization

added theorem unique_factorization_domain.unique

added structure unique_irreducible_factorization