Commit 2023-04-20 12:31 c80a95d4

View on Github →

feat: port RingTheory.ChainOfDivisors (#3056)

Estimated changes

Modified Mathlib.lean

Created Mathlib/RingTheory/ChainOfDivisors.lean

added theorem Associates.isAtom_iff

added theorem DivisorChain.card_subset_divisors_le_length_of_chain

added theorem DivisorChain.element_of_chain_eq_pow_second_of_chain

added theorem DivisorChain.element_of_chain_not_isUnit_of_index_ne_zero

added theorem DivisorChain.eq_pow_second_of_chain_of_has_chain

added theorem DivisorChain.eq_second_of_chain_of_prime_dvd

added theorem DivisorChain.exists_chain_of_prime_pow

added theorem DivisorChain.first_of_chain_isUnit

added theorem DivisorChain.isPrimePow_of_has_chain

added theorem DivisorChain.second_of_chain_is_irreducible

added theorem coe_factor_orderIso_map_eq_one_iff

added theorem factor_orderIso_map_one_eq_bot

added theorem map_prime_of_factor_orderIso

added theorem mem_normalizedFactors_factor_dvd_iso_of_mem_normalizedFactors

added theorem mem_normalizedFactors_factor_orderIso_of_mem_normalizedFactors

added def mkFactorOrderIsoOfFactorDvdEquiv

added theorem multiplicity_factor_dvd_iso_eq_multiplicity_of_mem_normalizedFactors

added theorem multiplicity_prime_eq_multiplicity_image_by_factor_orderIso

added theorem multiplicity_prime_le_multiplicity_image_by_factor_orderIso

added theorem pow_image_of_prime_by_factor_orderIso_dvd