mathlib

f6e9ec38 - chore(ring_theory/ideal/operations): generalise some typeclasses (#15200)

chore(ring_theory/ideal/operations): generalise some typeclasses (#15200) Using the generalisation linter mostly. Some more changes are possible surrounding map / comap, but they involve more restructuring, and I want to explore the right definitions of map and comap separately. All changes here are of the form: dropping commutativity, changing domain to no_zero_divisors (i.e. not assuming nontriviality), or dropping subtraction (ring to semiring).