Documentation
Carleson
.
ToMathlib
.
Analysis
.
RCLike
.
Basic
Search
return to top
source
Imports
Init
Mathlib.Analysis.RCLike.Basic
Imported by
RCLike
.
norm_I
source
theorem
RCLike
.
norm_I
{
K
:
Type
u_1}
[
RCLike
K
]
:
‖
I
‖
=
if
I
≠
0
then
1
else
0