Commit 2021-08-03 11:13 ad83714b
View on Github →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.