Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-03-18 20:21 8c89ae6f

View on Github →

feat(ring_theory/unique_factorization_domain): some lemmas relating shapes of factorisations (#9345) Given elements a, b in a unique_factorization_monoid, if there is an order-preserving bijection between the sets of factors of associates.mk a and associates.mk b then the prime factorisations of a and b have the same shape.

Estimated changes

Modified src/algebra/associated.lean

added theorem associates.is_atom_iff

added theorem dvd_prime_pow

Modified src/algebra/squarefree.lean

added theorem multiplicity.finite_prime_left

Created src/ring_theory/chain_of_divisors.lean

added theorem divisor_chain.card_subset_divisors_le_length_of_chain

added theorem divisor_chain.element_of_chain_eq_pow_second_of_chain

added theorem divisor_chain.element_of_chain_not_is_unit_of_index_ne_zero

added theorem divisor_chain.eq_pow_second_of_chain_of_has_chain

added theorem divisor_chain.eq_second_of_chain_of_prime_dvd

added theorem divisor_chain.exists_chain_of_prime_pow

added theorem divisor_chain.first_of_chain_is_unit

added theorem divisor_chain.is_prime_pow_of_has_chain

added theorem divisor_chain.second_of_chain_is_irreducible

added theorem multiplicity_prime_le_multiplicity_image_by_factor_order_iso

added theorem pow_image_of_prime_by_factor_order_iso_dvd

Modified src/ring_theory/ideal/operations.lean

added theorem ideal.comap_le_comap_iff_of_surjective

Modified src/ring_theory/multiplicity.lean

Modified src/ring_theory/unique_factorization_domain.lean

added theorem unique_factorization_monoid.exists_associated_prime_pow_of_unique_normalized_factor

added theorem unique_factorization_monoid.normalized_factors_of_irreducible_pow