Commit 2024-04-05 21:50 64e5ddf0
View on Github →chore(Field/InjSurj): Tidy (#11480)
Among other things, change the nsmul, zsmul, qsmul fields to have n/q come before x, because this matches the lemmas we want to write about them. It would be preferrable to perform the same changes to the AddMonoid/AddGroup-like typeclasses, but this is impossible with the current to_additive framework, so instead I have inserted some Function.swap at the interface between AddMonoid/AddGroup and Ring/Field.
Reduce the diff of #11203