feat(ring_theory/ideal/operations): add an instance (#6717)
This instance has been suggested by @eric-wieser in #6640.
On my machine I get a deterministic timeout in `ring_theory/finiteness` at line 325, but in principle it seems a useful instance to have.
Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
