Theorem normalized_factors_equiv_of_quot_equiv_multiplicity_eq_multiplicity
Modification history
2022-09-12 19:53
src/ring_theory/dedekind_domain/ideal.lean
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) …
Added normalized_factors_equiv_of_quot_equiv_multiplicity_eq_multiplicityView on Github →