Commit 2023-03-21 09:26 7c487d48

View on Github →

feat: port RingTheory.UniqueFactorizationDomain (#3003)

Estimated changes

Modified Mathlib.lean

Created Mathlib/RingTheory/UniqueFactorizationDomain.lean

added def Associates.BfactorSetMem

added theorem Associates.FactorSet.coe_add

added def Associates.FactorSet.prod

added theorem Associates.FactorSet.prod_eq_zero_iff

added theorem Associates.FactorSet.sup_add_inf_eq_add

added theorem Associates.FactorSet.unique

added def Associates.FactorSet.{u}

added def Associates.FactorSetMem

added def Associates.bcount

added theorem Associates.coprime_iff_inf_one

added def Associates.count

added theorem Associates.count_eq_zero_of_ne

added theorem Associates.count_factors_eq_find_of_dvd_pow

added theorem Associates.count_le_count_of_factors_le

added theorem Associates.count_le_count_of_le

added theorem Associates.count_mul

added theorem Associates.count_mul_of_coprime'

added theorem Associates.count_mul_of_coprime

added theorem Associates.count_ne_zero_iff_dvd

added theorem Associates.count_of_coprime

added theorem Associates.count_pow

added theorem Associates.count_reducible

added theorem Associates.count_self

added theorem Associates.count_some

added theorem Associates.count_zero

added theorem Associates.dvd_count_of_dvd_count_mul

added theorem Associates.dvd_count_pow

added theorem Associates.dvd_of_mem_factors'

added theorem Associates.dvd_of_mem_factors

added theorem Associates.eq_factors_of_eq_counts

added theorem Associates.eq_of_eq_counts

added theorem Associates.eq_of_factors_eq_factors

added theorem Associates.eq_of_prod_eq_prod

added theorem Associates.eq_pow_count_factors_of_dvd_pow

added theorem Associates.eq_pow_find_of_dvd_irreducible_pow

added theorem Associates.eq_pow_of_mul_eq_pow

added theorem Associates.exists_prime_dvd_of_not_inf_one

added theorem Associates.factorSetMem_eq_mem

added theorem Associates.factors'_cong

added theorem Associates.factors_0

added theorem Associates.factors_eq_none_iff_zero

added theorem Associates.factors_eq_some_iff_ne_zero

added theorem Associates.factors_le

added theorem Associates.factors_mk

added theorem Associates.factors_mono

added theorem Associates.factors_mul

added theorem Associates.factors_one

added theorem Associates.factors_prime_pow

added theorem Associates.factors_prod

added theorem Associates.factors_self

added theorem Associates.factors_subsingleton

added theorem Associates.is_pow_of_dvd_count

added theorem Associates.le_of_count_ne_zero

added theorem Associates.map_subtype_coe_factors'

added theorem Associates.mem_factorSet_some

added theorem Associates.mem_factorSet_top

added theorem Associates.mem_factors'_iff_dvd

added theorem Associates.mem_factors'_of_dvd

added theorem Associates.mem_factors_iff_dvd

added theorem Associates.mem_factors_of_dvd

added theorem Associates.pow_factors

added theorem Associates.prime_pow_dvd_iff_le

added theorem Associates.prod_add

added theorem Associates.prod_coe

added theorem Associates.prod_factors

added theorem Associates.prod_le

added theorem Associates.prod_le_prod_iff_le

added theorem Associates.prod_mono

added theorem Associates.prod_top

added theorem Associates.quot_out

added theorem Associates.reducible_not_mem_factorSet

added theorem Associates.sup_mul_inf

added theorem Associates.unique'

added theorem Irreducible.normalizedFactors_pow

added theorem MulEquiv.uniqueFactorizationMonoid

added theorem MulEquiv.uniqueFactorizationMonoid_iff

added theorem UniqueFactorizationMonoid.associated_iff_normalizedFactors_eq_normalizedFactors

added theorem UniqueFactorizationMonoid.count_normalizedFactors_eq'

added theorem UniqueFactorizationMonoid.count_normalizedFactors_eq

added theorem UniqueFactorizationMonoid.dvdNotUnit_iff_normalizedFactors_lt_normalizedFactors

added theorem UniqueFactorizationMonoid.dvd_iff_normalizedFactors_le_normalizedFactors

added theorem UniqueFactorizationMonoid.dvd_of_dvd_mul_left_of_no_prime_factors

added theorem UniqueFactorizationMonoid.dvd_of_dvd_mul_right_of_no_prime_factors

added theorem UniqueFactorizationMonoid.dvd_of_mem_factors

added theorem UniqueFactorizationMonoid.dvd_of_mem_normalizedFactors

added theorem UniqueFactorizationMonoid.exists_associated_prime_pow_of_unique_normalized_factor

added theorem UniqueFactorizationMonoid.exists_mem_factors

added theorem UniqueFactorizationMonoid.exists_mem_factors_of_dvd

added theorem UniqueFactorizationMonoid.exists_mem_normalizedFactors

added theorem UniqueFactorizationMonoid.exists_mem_normalizedFactors_of_dvd

added theorem UniqueFactorizationMonoid.exists_prime_factors

added theorem UniqueFactorizationMonoid.exists_reduced_factors'

added theorem UniqueFactorizationMonoid.exists_reduced_factors

added theorem UniqueFactorizationMonoid.factors_eq_normalizedFactors

added theorem UniqueFactorizationMonoid.factors_mul

added theorem UniqueFactorizationMonoid.factors_one

added theorem UniqueFactorizationMonoid.factors_pos

added theorem UniqueFactorizationMonoid.factors_pow

added theorem UniqueFactorizationMonoid.factors_prod

added theorem UniqueFactorizationMonoid.factors_unique

added theorem UniqueFactorizationMonoid.factors_zero

added theorem UniqueFactorizationMonoid.iff_exists_prime_factors

added theorem UniqueFactorizationMonoid.induction_on_coprime

added theorem UniqueFactorizationMonoid.induction_on_prime

added theorem UniqueFactorizationMonoid.induction_on_prime_power

added theorem UniqueFactorizationMonoid.irreducible_of_factor

added theorem UniqueFactorizationMonoid.irreducible_of_normalized_factor

added theorem UniqueFactorizationMonoid.le_multiplicity_iff_replicate_le_normalizedFactors

added theorem UniqueFactorizationMonoid.mem_normalizedFactors_eq_of_associated

added theorem UniqueFactorizationMonoid.multiplicative_of_coprime

added theorem UniqueFactorizationMonoid.multiplicative_prime_power

added theorem UniqueFactorizationMonoid.multiplicity_eq_count_normalizedFactors

added theorem UniqueFactorizationMonoid.ne_zero_of_mem_factors

added theorem UniqueFactorizationMonoid.no_factors_of_no_prime_factors

added theorem UniqueFactorizationMonoid.normalize_normalized_factor

added theorem UniqueFactorizationMonoid.normalizedFactors_eq_of_dvd

added theorem UniqueFactorizationMonoid.normalizedFactors_irreducible

added theorem UniqueFactorizationMonoid.normalizedFactors_mul

added theorem UniqueFactorizationMonoid.normalizedFactors_of_irreducible_pow

added theorem UniqueFactorizationMonoid.normalizedFactors_one

added theorem UniqueFactorizationMonoid.normalizedFactors_pos

added theorem UniqueFactorizationMonoid.normalizedFactors_pow

added theorem UniqueFactorizationMonoid.normalizedFactors_prod

added theorem UniqueFactorizationMonoid.normalizedFactors_prod_eq

added theorem UniqueFactorizationMonoid.normalizedFactors_prod_of_prime

added theorem UniqueFactorizationMonoid.normalizedFactors_zero

added theorem UniqueFactorizationMonoid.of_exists_prime_factors

added theorem UniqueFactorizationMonoid.of_exists_unique_irreducible_factors

added theorem UniqueFactorizationMonoid.pow_eq_pow_iff

added theorem UniqueFactorizationMonoid.pow_right_injective

added theorem UniqueFactorizationMonoid.prime_of_factor

added theorem UniqueFactorizationMonoid.prime_of_normalized_factor

added theorem UniqueFactorizationMonoid.prime_pow_coprime_prod_of_coprime_insert

added theorem UniqueFactorizationMonoid.zero_not_mem_normalizedFactors

added theorem WfDvdMonoid.exists_factors

added theorem WfDvdMonoid.exists_irreducible_factor

added theorem WfDvdMonoid.iff_wellFounded_associates

added theorem WfDvdMonoid.induction_on_irreducible

added theorem WfDvdMonoid.not_unit_iff_exists_factors_eq

added theorem WfDvdMonoid.of_exists_prime_factors

added theorem WfDvdMonoid.of_wellFounded_associates

added theorem WfDvdMonoid.of_wfDvdMonoid_associates

added theorem WfDvdMonoid.wellFounded_associates

added theorem associated_of_factorization_eq

added theorem factorization_eq_count

added theorem factorization_mul

added theorem factorization_one

added theorem factorization_pow

added theorem factorization_zero

added theorem irreducible_iff_prime_of_exists_prime_factors

added theorem irreducible_iff_prime_of_exists_unique_irreducible_factors

added theorem prime_factors_irreducible

added theorem prime_factors_unique

added theorem support_factorization

added theorem ufm_of_gcd_of_wfDvdMonoid