Commit 2021-07-22 16:15 7cdd7020

chore(ring_theory): set_like instance for fractional ideals (#8275) This PR does a bit of cleanup in fractional_ideal.lean by using set_like to define has_mem and the coe to set. As a bonus, it removes the namespace ring at the top of the file, that has been bugging me ever after I added it in the original fractional ideal PR.