Theorem Int.coe_negOnePow_natCast

Modification history

2024-10-20 21:29
Mathlib/Algebra/Ring/NegOnePow.lean
feat: `negOnePow n = (-1 : ℤ) ^ n` (#17967) …
Added Int.coe_negOnePow_natCastView on Github →