Documentation

Mathlib.Algebra.Field.NegOnePow

Integer powers of -1 in a field #

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