mathlib

34aa23af - feat(ring_theory/dedekind_domain): connect (/) and (⁻¹) on fractional ideals (#9808)

feat(ring_theory/dedekind_domain): connect (/) and (⁻¹) on fractional ideals (#9808) Turns out we never actually proved the `div_eq_mul_inv` lemma on fractional ideals, which motivated the entire definition of `div_inv_monoid`. So here it is, along with some useful supporting lemmas.