mathlib

1dc4bef9 - feat(ring_theory): shortcut lemmas for `coe : ideal R → fractional_ideal R⁰ K` (#8395)

feat(ring_theory): shortcut lemmas for `coe : ideal R → fractional_ideal R⁰ K` (#8395) These results were already available, but in a less convenient form that e.g. asked you to prove an inclusion of submonoids `S ≤ R⁰`. Specializing them to the common case where the fractional ideal is in the field of fractions should save a bit of headache in the common cases.