mathlib

b112d4dd - refactor(ring_theory/ideal/operations): generalize various definitions to remove negation and commutativity (#9737)

refactor(ring_theory/ideal/operations): generalize various definitions to remove negation and commutativity (#9737) Mostly this just weakens assumptions in `variable`s lines, but occasionally this moves lemmas to a more appropriate section too.