Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
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
- Loading branch information
1 parent
1b545f0
commit 64e5ddf
Showing
16 changed files
with
496 additions
and
603 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Oops, something went wrong.