Commit 2026-02-27 10:47 57e06661
View on Github →feat(Algebra/Ring/NegOnePow): add negOnePow ↔ natAbs bridge lemmas (#34944)
Adds Int.cast_negOnePow_eq_neg_one_pow_natAbs (for any Ring R) and its ℤ specialization Int.coe_negOnePow_eq_neg_one_pow_natAbs, relating negOnePow n to (-1) ^ n.natAbs.
The file already has cast_negOnePow_natCast for n : ℕ but nothing for general integers via natAbs.