Commit 2022-12-19 15:36 80b4179a

View on Github →

feat: port Algebra.Parity (#1092) dcf2250875895376a142faeeac5eabff32c48655

Estimated changes

added theorem Even.add_odd
added theorem Even.isSquare_pow
added theorem Even.isSquare_zpow
added theorem Even.mul_left
added theorem Even.mul_right
added theorem Even.neg_one_pow
added theorem Even.neg_one_zpow
added theorem Even.neg_pow
added theorem Even.neg_zpow
added theorem Even.pow_abs
added theorem Even.pow_nonneg
added theorem Even.pow_of_ne_zero
added theorem Even.pow_pos
added theorem Even.pow_pos_iff
added theorem Even.sub_odd
added theorem Even.tsub
added theorem IsSquare.div
added theorem IsSquare.map
added theorem IsSquare.mul
added theorem IsSquare.pow
added theorem IsSquare.zpow
added def IsSquare
added theorem IsSquare_sq
added theorem Odd.add_even
added theorem Odd.add_odd
added theorem Odd.map
added theorem Odd.mul
added theorem Odd.neg
added theorem Odd.neg_one_pow
added theorem Odd.neg_pow
added theorem Odd.pos
added theorem Odd.pow
added theorem Odd.pow_neg
added theorem Odd.pow_neg_iff
added theorem Odd.pow_nonneg_iff
added theorem Odd.pow_nonpos
added theorem Odd.pow_nonpos_iff
added theorem Odd.pow_pos_iff
added theorem Odd.strict_mono_pow
added theorem Odd.sub_even
added theorem Odd.sub_odd
added def Odd
added theorem even_abs
added theorem even_bit0
added theorem even_iff_exists_bit0
added theorem even_iff_two_dvd
added theorem even_neg_two
added theorem even_two
added theorem even_two_mul
added theorem isSquare_iff_exists_sq
added theorem isSquare_inv
added theorem isSquare_mul_self
added theorem isSquare_one
added theorem isSquare_op_iff
added theorem isSquare_zero
added theorem odd_abs
added theorem odd_bit1
added theorem odd_iff_exists_bit1
added theorem odd_neg
added theorem odd_neg_one
added theorem odd_one
added theorem odd_two_mul_add_one
added theorem pow_bit0_abs
added theorem range_two_mul
added theorem range_two_mul_add_one