Documentation
Mathlib
.
Algebra
.
Field
.
NegOnePow
Search
return to top
source
Imports
Init
Mathlib.Tactic.NormNum
Mathlib.Algebra.Field.Defs
Mathlib.Algebra.Ring.NegOnePow
Imported by
Int
.
cast_negOnePow
Integer powers of
-1
in a field
#
source
theorem
Int
.
cast_negOnePow
(
K
:
Type
u_1)
(
n
:
ℤ
)
[
DivisionRing
K
]
:
↑
↑
n
.
negOnePow
=
(-
1
)
^
n