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.