Documentation
LeanAPAP
.
Mathlib
.
Analysis
.
RCLike
.
Basic
Search
return to top
source
Imports
Init
Mathlib.Analysis.RCLike.Basic
Imported by
RCLike
.
enorm_ofReal
source
@[simp]
theorem
RCLike
.
enorm_ofReal
{
K
:
Type
u_1}
[
RCLike
K
]
(
r
:
ℝ
)
:
‖
↑
r
‖ₑ
=
‖
r
‖ₑ