Commit 2024-03-15 12:53 d7e49441

View on Github →

fix: remove DecidableEq assumption from factors (#11158) It doesn't make a lot of sense for factors to require a DecidableEq assumption since it's not used in the statement, and the definition is already noncomputable. This PR removes that assumption and updates some lemmas later in the file accordingly.

Estimated changes

Modified Mathlib/RingTheory/ChainOfDivisors.lean

modified theorem map_prime_of_factor_orderIso

modified theorem mem_normalizedFactors_factor_dvd_iso_of_mem_normalizedFactors

modified theorem mem_normalizedFactors_factor_orderIso_of_mem_normalizedFactors

modified theorem multiplicity_prime_eq_multiplicity_image_by_factor_orderIso

modified theorem multiplicity_prime_le_multiplicity_image_by_factor_orderIso

Modified Mathlib/RingTheory/DedekindDomain/Ideal.lean

modified theorem Ideal.factors_span_eq

Modified Mathlib/RingTheory/DedekindDomain/PID.lean

modified theorem IsLocalization.OverPrime.mem_normalizedFactors_of_isPrime

Modified Mathlib/RingTheory/UniqueFactorizationDomain.lean

modified theorem Associates.count_eq_zero_of_ne

modified theorem Associates.count_factors_eq_find_of_dvd_pow

modified theorem Associates.count_le_count_of_factors_le

modified theorem Associates.count_le_count_of_le

modified theorem Associates.count_mul

modified theorem Associates.count_mul_of_coprime'

modified theorem Associates.count_mul_of_coprime

modified theorem Associates.count_ne_zero_iff_dvd

modified theorem Associates.count_of_coprime

modified theorem Associates.count_pow

modified theorem Associates.count_self

modified theorem Associates.dvd_count_of_dvd_count_mul

modified theorem Associates.dvd_count_pow

modified theorem Associates.eq_factors_of_eq_counts

modified theorem Associates.eq_of_eq_counts

modified theorem Associates.eq_pow_count_factors_of_dvd_pow

modified theorem Associates.is_pow_of_dvd_count

modified theorem Associates.le_of_count_ne_zero

modified theorem Associates.prime_pow_dvd_iff_le

modified theorem UniqueFactorizationMonoid.factors_eq_normalizedFactors

modified theorem UniqueFactorizationMonoid.factors_pow_count_prod

modified theorem UniqueFactorizationMonoid.le_multiplicity_iff_replicate_le_normalizedFactors