Theorem: norm_innerSL_le_one (ForML/Util.lean)

State before:
𝕜 : Type u_1
inst✝² : IsROrC 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
⊢ ‖innerSL 𝕜‖ ≤ 1
Tactic:
simp [ContinuousLinearMap.opNorm_le_iff]
State after:
no goals