Commit 2023-03-17 19:18 acebd8d4
View on Github →feat(algebra/*/opposite): Missing instances (#18602)
A few missing instances about nat.cast/int.cast/rat.cast and mul_opposite/add_opposite.
Also add the (weirdly) missing add_comm_group_with_one → add_comm_monoid_with_one.
Finally, this changes the defeq of rat.cast on mul_opposite to be simpler.