Documentation
ClassFieldTheory
.
Mathlib
.
Data
.
Int
.
WithZero
Search
return to top
source
Imports
Init
Mathlib.Data.Int.WithZero
Imported by
WithZeroMulInt
.
toNNReal_exp
source
@[simp]
theorem
WithZeroMulInt
.
toNNReal_exp
{
e
:
NNReal
}
(
he
:
e
≠
0
)
{
n
:
ℤ
}
:
(
toNNReal
he
)
(
WithZero.exp
n
)
=
e
^
n