Mathlib v3 is deprecated. Go to Mathlib v4

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_muls and even_iff_two_dvds in a few places where the defeq to the divisibility by 2 was exploited. Zulip discussion

Estimated changes

deleted theorem add_monoid_hom.even
deleted theorem even.add_even
deleted theorem even.sub_even
deleted def even
modified theorem even_abs
modified theorem even_iff_two_dvd
deleted theorem even_neg
modified theorem even_neg_two
modified theorem even_two
modified theorem even_two_mul
deleted theorem even_zero
added theorem is_square.map
added def is_square
added theorem is_square_inv
added theorem is_square_mul_self
added theorem is_square_one
added theorem is_square_op_iff
added theorem is_square_sq
modified theorem odd_abs
modified theorem int.div_two_mul_two_of_even
modified theorem int.two_mul_div_two_of_even
modified theorem nat.div_two_mul_two_of_even
modified theorem nat.two_mul_div_two_of_even
modified theorem int.not_is_field