Norm properties of the extension of continuous ℝ-linear functionals to 𝕜-linear functionals

This file shows that ContinuousLinearMap.extendTo𝕜 preserves the norm of the functional.

theorem ContinuousLinearMap.norm_extendTo𝕜'_bound {𝕜 : Type u_1} {F : Type u_2} [RCLike 𝕜] [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] [NormedSpace ℝ F] [IsScalarTower ℝ 𝕜 F] (fr : StrongDual ℝ F) (x : F) : ‖(extendTo𝕜' fr) x‖ ≤ ‖fr‖ * ‖x‖

The norm of the extension is bounded by ‖fr‖.

@[simp]

theorem ContinuousLinearMap.norm_extendTo𝕜' {𝕜 : Type u_1} {F : Type u_2} [RCLike 𝕜] [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] [NormedSpace ℝ F] [IsScalarTower ℝ 𝕜 F] (fr : StrongDual ℝ F) : ‖extendTo𝕜' fr‖ = ‖fr‖

@[simp]

theorem ContinuousLinearMap.norm_extendTo𝕜 {𝕜 : Type u_1} {F : Type u_2} [RCLike 𝕜] [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] (fr : StrongDual ℝ (RestrictScalars ℝ 𝕜 F)) : ‖extendTo𝕜 fr‖ = ‖fr‖