Integer powers of -1 in a field

theorem Int.cast_negOnePow (K : Type u_1) (n : ℤ) [Field K] : ↑↑n.negOnePow = (-1) ^ n

@[deprecated Int.cast_negOnePow (since := "2024-10-20")]

theorem Int.coe_negOnePow (K : Type u_1) (n : ℤ) [Field K] : ↑↑n.negOnePow = (-1) ^ n

Alias of Int.cast_negOnePow.