Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-05-17 21:17 0afb90b4

View on Github →

refactor(algebra/parity): Generalize to division monoids (#14187) Generalize lemmas about is_square, even and odd. Improve dot notation.

Estimated changes

modified def mul_equiv.inv'
modified theorem even.add_odd
modified theorem even.neg_one_zpow
modified theorem even.neg_zpow
added theorem even.tsub
deleted theorem even.tsub_even
modified theorem even_abs
added theorem is_square.div
deleted theorem is_square.div_is_square
added theorem is_square.mul
deleted theorem is_square.mul_is_square
modified def is_square
modified theorem is_square_iff_exists_sq
modified theorem is_square_inv
modified theorem is_square_mul_self
modified theorem is_square_op_iff
modified theorem odd.add_odd
added theorem odd.map
added theorem odd.mul
deleted theorem odd.mul_odd
modified theorem odd_abs
modified theorem odd_neg
deleted theorem ring_hom.odd