Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-07-15 18:31 f6e9ec38

View on Github →

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).

Estimated changes