Commit 2025-04-19 15:55 6a858d8e
View on Github →feat: (-1) ^ m = (-1) ^ n (#24160)
- add
neg_one_pow_congr; - prove a lemma about parity of
Fin.succAbove i j + Fin.predAbove j i. Backported (with adjusted API) from https://github.com/urkud/DeRhamCohomology