Commit 2022-04-06 12:59 138448ae
View on Github →feat(algebra/parity): introduce is_square
and, via to_additive
, also even
(#13037)
This PR continues the refactor began in #12882. Now that most of the the even/odd lemmas are in the same file, I changed the definition of even
to become the to_additive
version of is_square
.
The reason for the large number of files touched is that the definition of even
actually changed, from being of the form 2 * n
to being of the form n + n
. Thus, I inserted appropriate two_mul
s and even_iff_two_dvd
s in a few places where the defeq to the divisibility by 2 was exploited.
Zulip discussion