English
The operator norm of the left-scalar-multiplication operator lsmul 𝕜 R is exactly 1.
Русский
Норма оператора левого умножения lsmul 𝕜 R ровна единице.
LaTeX
$$$\\|\\mathrm{lsmul}_{\\mathbb{K},R}\\| = 1$$$
Lean4
/-- The norm of `lsmul` equals 1 in any nontrivial normed group.
This is `ContinuousLinearMap.opNorm_lsmul_le` as an equality. -/
@[simp]
theorem opNorm_lsmul [NormedField R] [NormedAlgebra 𝕜 R] [NormedSpace R E] [IsScalarTower 𝕜 R E] [Nontrivial E] :
‖(lsmul 𝕜 R : R →L[𝕜] E →L[𝕜] E)‖ = 1 :=
by
refine ContinuousLinearMap.opNorm_eq_of_bounds zero_le_one (fun x => ?_) fun N _ h => ?_
· rw [one_mul]
apply opNorm_lsmul_apply_le
obtain ⟨y, hy⟩ := exists_ne (0 : E)
refine le_of_mul_le_mul_right ?_ (norm_pos_iff.mpr hy)
simpa using le_of_opNorm_le _ (h 1) y
