Commit 2024-12-29 12:22 68fbd252

View on Github →

feat: (-1 : R) ^ n = ite (Even n) 1 (-1) (#20320)

Estimated changes

added theorem neg_one_pow_eq_ite