Commit 2021-07-26 15:58 1dc4bef9

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.