mathlib

25972642 - chore(ring_theory/ideal/operations): golf a definition using new actions (#9152)

chore(ring_theory/ideal/operations): golf a definition using new actions (#9152) This action can be expressed more directly in terms of other actions, without the unfolded definition changing.