Commit 2022-09-12 19:53 36e01301

View on Github →

feat(ring_theory/dedekind_domain/ideal): construct map between the sets of prime factors of ideal I and J induced by an isomorphism between R/I and S/J (#16455) These lemmas generalize results that were originally in #15000.

Estimated changes

Modified src/ring_theory/dedekind_domain/ideal.lean

modified def ideal_factors_equiv_of_quot_equiv

added theorem ideal_factors_equiv_of_quot_equiv_is_dvd_iso

added theorem ideal_factors_equiv_of_quot_equiv_mem_normalized_factors_of_mem_normalized_factors

added theorem ideal_factors_equiv_of_quot_equiv_symm

added theorem multiplicity_normalized_factors_equiv_span_normalized_factors_eq_multiplicity

added theorem multiplicity_normalized_factors_equiv_span_normalized_factors_symm_eq_multiplicity

added def normalized_factors_equiv_of_quot_equiv

added theorem normalized_factors_equiv_of_quot_equiv_multiplicity_eq_multiplicity

added theorem normalized_factors_equiv_of_quot_equiv_symm