mathlib3

ad83714b - feat(fractional_ideal): `coe : ideal → fractional_ideal` as ring hom (#8511)

feat(fractional_ideal): `coe : ideal → fractional_ideal` as ring hom (#8511) This PR bundles the coercion from integral ideals to fractional ideals as a ring hom, and proves the missing `simp` lemmas that show the map indeed preserves the ring structure. Co-authored-by: Anne Baanen <Vierkantor@users.noreply.github.com>