Mathlib Changelog
v4
Changelog
About
Github
Commit
2022-12-19 15:36
80b4179a
View on Github →
feat: port Algebra.Parity (
#1092
) dcf2250875895376a142faeeac5eabff32c48655
depends on:
#1055
Estimated changes
Modified
Mathlib.lean
Created
Mathlib/Algebra/Parity.lean
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_exists_two_mul
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