mathlib3

6fe0c3b1 - refactor(algebra/group/to_additive + files containing even/odd): move many lemmas involving even/odd to the same file (#12882)

refactor(algebra/group/to_additive + files containing even/odd): move many lemmas involving even/odd to the same file (#12882) This is the first step in refactoring the definition of `even` to be the `to_additive` of `square`. This PR simply gathers together many (though not all) lemmas that involve `even` or `odd` in their assumptions. The choice of which lemmas to migrate to the file `algebra.parity` was dictated mostly by whether importing `algebra.parity` in the current home would create a cyclic import. The only change that is not a simple shift from a file to another one is the addition in `to_additive` for support to change `square` in a multiplicative name to `even` in an additive name. The change to the test file `test.ring` is due to the fact that the definition of `odd` was no longer imported by the file.