Commit 2022-03-28 16:49 6fe0c3b1

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.