Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-10-12 14:57 b3ce8837

View on Github →

feat(algebra/*_power): simplify (-a)^(bit0 _) and (-a)^(bit1 _) (#4573) Works for pow and fpow. Also simplify powers of I : ℂ.

Estimated changes

added theorem neg_fpow_bit0
added theorem neg_fpow_bit1
added theorem bit0_nsmul'
added theorem bit1_nsmul'
added theorem neg_pow_bit0
added theorem neg_pow_bit1
added theorem pow_bit0'
added theorem pow_bit1'
added theorem fpow_add'
added theorem fpow_bit0'
added theorem fpow_bit0
added theorem fpow_bit1'
added theorem fpow_bit1
added theorem complex.I_fpow_bit0
added theorem complex.I_fpow_bit1
added theorem complex.I_pow_bit0
added theorem complex.I_pow_bit1
added theorem int.bit0_ne_bit1
added theorem int.bit1_ne_bit0
added theorem int.bit1_ne_zero
added theorem int.bodd_bit0
added theorem int.bodd_bit1
modified theorem int.bodd_two