Commit 2024-04-20 17:51 cd502bdf

View on Github →

feat: Generalise sign of power lemmas (#12289)

Estimated changes

Modified Mathlib/Algebra/Parity.lean

modified theorem Even.pow_pos

added theorem Odd.pow_add_pow_eq_zero

deleted theorem Odd.pow_neg

modified theorem Odd.pow_neg_iff

deleted theorem Odd.pow_nonpos

modified theorem Odd.pow_nonpos_iff

modified theorem Odd.strictMono_pow