Theorem neg_one_pow_eq_ite

Modification history

2025-04-19 15:55
Mathlib/Algebra/Ring/Parity.lean
feat: `(-1) ^ m = (-1) ^ n` (#24160) …
Modified neg_one_pow_eq_iteView on Github →
2024-12-29 12:22
Mathlib/Algebra/Ring/Parity.lean
feat: `(-1 : R) ^ n = ite (Even n) 1 (-1)` (#20320)
Added neg_one_pow_eq_iteView on Github →