Documentation
Init
.
Data
.
Int
.
Pow
Search
return to top
source
Imports
Init.Data.Int.Lemmas
Init.Data.Nat.Lemmas
Imported by
Int
.
pow_zero
Int
.
pow_succ
Int
.
pow_succ'
Int
.
pow_pos
Int
.
pow_nonneg
Int
.
pow_ne_zero
Int
.
pow_le_pow_of_le_left
Int
.
pow_le_pow_of_le_right
Int
.
pos_pow_of_pos
Int
.
natCast_pow
Int
.
two_pow_pred_sub_two_pow
Int
.
two_pow_pred_sub_two_pow'
Int
.
pow_lt_pow_of_lt
Int
.
natAbs_pow
Int
.
toNat_pow_of_nonneg
pow
#
source
@[simp]
theorem
Int
.
pow_zero
(
b
:
Int
)
:
b
^
0
=
1
source
theorem
Int
.
pow_succ
(
b
:
Int
)
(
e
:
Nat
)
:
b
^
(
e
+
1
)
=
b
^
e
*
b
source
theorem
Int
.
pow_succ'
(
b
:
Int
)
(
e
:
Nat
)
:
b
^
(
e
+
1
)
=
b
*
b
^
e
source
theorem
Int
.
pow_pos
{
n
:
Int
}
{
m
:
Nat
}
:
0
<
n
→
0
<
n
^
m
source
theorem
Int
.
pow_nonneg
{
n
:
Int
}
{
m
:
Nat
}
:
0
≤
n
→
0
≤
n
^
m
source
theorem
Int
.
pow_ne_zero
{
n
:
Int
}
{
m
:
Nat
}
:
n
≠
0
→
n
^
m
≠
0
source
@[reducible, inline, deprecated Nat.pow_le_pow_left (since := "2025-02-17")]
abbrev
Int
.
pow_le_pow_of_le_left
{
n
m
:
Nat
}
(
h
:
n
≤
m
)
(
i
:
Nat
)
:
n
^
i
≤
m
^
i
Equations
Instances For
source
@[reducible, inline, deprecated Nat.pow_le_pow_right (since := "2025-02-17")]
abbrev
Int
.
pow_le_pow_of_le_right
{
n
:
Nat
}
(
hx
:
n
>
0
)
{
i
j
:
Nat
}
:
i
≤
j
→
n
^
i
≤
n
^
j
Equations
Instances For
source
@[reducible, inline, deprecated Nat.pow_pos (since := "2025-02-17")]
abbrev
Int
.
pos_pow_of_pos
{
a
n
:
Nat
}
(
h
:
0
<
a
)
:
0
<
a
^
n
Equations
Instances For
source
@[simp]
theorem
Int
.
natCast_pow
(
b
n
:
Nat
)
:
↑(
b
^
n
)
=
↑
b
^
n
source
@[simp]
theorem
Int
.
two_pow_pred_sub_two_pow
{
w
:
Nat
}
(
h
:
0
<
w
)
:
↑(
2
^
(
w
-
1
))
-
↑(
2
^
w
)
=
-
↑(
2
^
(
w
-
1
))
source
@[simp]
theorem
Int
.
two_pow_pred_sub_two_pow'
{
w
:
Nat
}
(
h
:
0
<
w
)
:
2
^
(
w
-
1
)
-
2
^
w
=
-
2
^
(
w
-
1
)
source
theorem
Int
.
pow_lt_pow_of_lt
{
a
:
Int
}
{
b
c
:
Nat
}
(
ha
:
1
<
a
)
(
hbc
:
b
<
c
)
:
a
^
b
<
a
^
c
source
@[simp]
theorem
Int
.
natAbs_pow
(
n
:
Int
)
(
k
:
Nat
)
:
(
n
^
k
).
natAbs
=
n
.
natAbs
^
k
source
theorem
Int
.
toNat_pow_of_nonneg
{
x
:
Int
}
(
h
:
0
≤
x
)
(
k
:
Nat
)
:
(
x
^
k
).
toNat
=
x
.
toNat
^
k