mathlib3
7cdd7020 - chore(ring_theory): `set_like` instance for fractional ideals (#8275)

Commit
4 years ago
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. Co-authored-by: Anne Baanen <Vierkantor@users.noreply.github.com>
Author
Parents
Loading