Commit 2023-09-04 17:35 2f410e1e

View on Github →

feat(Algebra): integer powers of -1 (#6720) This PR introduces the map Int.negOnePow : ℤ → ℤ which sends n to (-1 : Units ℤ) ^ n.

Estimated changes

added def Int.negOnePow
added theorem Int.negOnePow_add
added theorem Int.negOnePow_def
added theorem Int.negOnePow_eq_iff
added theorem Int.negOnePow_even
added theorem Int.negOnePow_mul_self
added theorem Int.negOnePow_neg
added theorem Int.negOnePow_odd
added theorem Int.negOnePow_one
added theorem Int.negOnePow_sub
added theorem Int.negOnePow_succ
added theorem Int.negOnePow_two_mul
added theorem Int.negOnePow_zero