@[simp]

theorem ContinuousLinearMap.opNNNorm_comp_linearIsometryEquiv {𝕜₁ : Type u_1} {𝕜₂ : Type u_2} {𝕜₃ : Type u_3} {E : Type u_4} {F : Type u_5} {G : Type u_6} [NontriviallyNormedField 𝕜₁] [NormedAddCommGroup E] [NormedSpace 𝕜₁ E] [NontriviallyNormedField 𝕜₂] [NormedAddCommGroup F] [NormedSpace 𝕜₂ F] [NontriviallyNormedField 𝕜₃] [NormedAddCommGroup G] [NormedSpace 𝕜₃ G] {σ₁₂ : 𝕜₁ →+* 𝕜₂} {σ₂₁ : 𝕜₂ →+* 𝕜₁} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] {σ₂₃ : 𝕜₂ →+* 𝕜₃} {σ₁₃ : 𝕜₁ →+* 𝕜₃} [RingHomIsometric σ₁₃] [RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] [RingHomIsometric σ₂₃] (f : F →SL[σ₂₃] G) (e : E ≃ₛₗᵢ[σ₁₂] F) : ‖f ∘SL ↑↑e‖₊ = ‖f‖₊

Postcomposition with a linear isometry preserves the operator norm.

@[simp]

theorem ContinuousLinearMap.opNNNorm_linearIsometryEquiv_comp {𝕜₁ : Type u_1} {𝕜₂ : Type u_2} {𝕜₃ : Type u_3} {E : Type u_4} {F : Type u_5} {G : Type u_6} [NontriviallyNormedField 𝕜₁] [NormedAddCommGroup E] [NormedSpace 𝕜₁ E] [NontriviallyNormedField 𝕜₂] [NormedAddCommGroup F] [NormedSpace 𝕜₂ F] [NontriviallyNormedField 𝕜₃] [NormedAddCommGroup G] [NormedSpace 𝕜₃ G] {σ₁₂ : 𝕜₁ →+* 𝕜₂} {σ₂₃ : 𝕜₂ →+* 𝕜₃} {σ₃₂ : 𝕜₃ →+* 𝕜₂} [RingHomInvPair σ₂₃ σ₃₂] [RingHomInvPair σ₃₂ σ₂₃] {σ₁₃ : 𝕜₁ →+* 𝕜₃} [RingHomIsometric σ₁₃] [RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] [RingHomIsometric σ₁₂] (e : F ≃ₛₗᵢ[σ₂₃] G) (f : E →SL[σ₁₂] F) : ‖↑↑e ∘SL f‖₊ = ‖f‖₊

Postcomposition with a linear isometry preserves the operator norm.

@[simp]

theorem ContinuousLinearMap.opNorm_comp_linearIsometryEquiv' {𝕜₁ : Type u_1} {𝕜₂ : Type u_2} {𝕜₃ : Type u_3} {E : Type u_4} {F : Type u_5} {G : Type u_6} [NontriviallyNormedField 𝕜₁] [NormedAddCommGroup E] [NormedSpace 𝕜₁ E] [NontriviallyNormedField 𝕜₂] [NormedAddCommGroup F] [NormedSpace 𝕜₂ F] [NontriviallyNormedField 𝕜₃] [NormedAddCommGroup G] [NormedSpace 𝕜₃ G] {σ₁₂ : 𝕜₁ →+* 𝕜₂} {σ₂₁ : 𝕜₂ →+* 𝕜₁} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] {σ₂₃ : 𝕜₂ →+* 𝕜₃} {σ₁₃ : 𝕜₁ →+* 𝕜₃} [RingHomIsometric σ₁₃] [RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] [RingHomIsometric σ₂₃] (f : F →SL[σ₂₃] G) (e : E ≃ₛₗᵢ[σ₁₂] F) : ‖f ∘SL ↑↑e‖ = ‖f‖

Postcomposition with a linear isometry preserves the operator norm.

@[simp]

theorem ContinuousLinearMap.opNorm_linearIsometryEquiv_comp {𝕜₁ : Type u_1} {𝕜₂ : Type u_2} {𝕜₃ : Type u_3} {E : Type u_4} {F : Type u_5} {G : Type u_6} [NontriviallyNormedField 𝕜₁] [NormedAddCommGroup E] [NormedSpace 𝕜₁ E] [NontriviallyNormedField 𝕜₂] [NormedAddCommGroup F] [NormedSpace 𝕜₂ F] [NontriviallyNormedField 𝕜₃] [NormedAddCommGroup G] [NormedSpace 𝕜₃ G] {σ₁₂ : 𝕜₁ →+* 𝕜₂} {σ₂₃ : 𝕜₂ →+* 𝕜₃} {σ₃₂ : 𝕜₃ →+* 𝕜₂} [RingHomInvPair σ₂₃ σ₃₂] [RingHomInvPair σ₃₂ σ₂₃] {σ₁₃ : 𝕜₁ →+* 𝕜₃} [RingHomIsometric σ₁₃] [RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] [RingHomIsometric σ₁₂] (e : F ≃ₛₗᵢ[σ₂₃] G) (f : E →SL[σ₁₂] F) : ‖↑↑e ∘SL f‖ = ‖f‖

Postcomposition with a linear isometry preserves the operator norm.

@[simp]

theorem ContinuousLinearMap.opNNNorm_mul_linearIsometryEquiv {𝕜 : Type u_7} {E : Type u_8} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] (f : E →L[𝕜] E) (e : E ≃ₗᵢ[𝕜] E) : ‖f * ↑↑e‖₊ = ‖f‖₊

Postcomposition with a linear isometry preserves the operator norm.

@[simp]

theorem ContinuousLinearMap.opNNNorm_linearIsometryEquiv_mul {𝕜 : Type u_7} {E : Type u_8} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] (e : E ≃ₗᵢ[𝕜] E) (f : E →L[𝕜] E) : ‖↑↑e * f‖₊ = ‖f‖₊

Postcomposition with a linear isometry preserves the operator norm.

@[simp]

theorem ContinuousLinearMap.opNorm_mul_linearIsometryEquiv {𝕜 : Type u_7} {E : Type u_8} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] (f : E →L[𝕜] E) (e : E ≃ₗᵢ[𝕜] E) : ‖f * ↑↑e‖ = ‖f‖

Postcomposition with a linear isometry preserves the operator norm.

@[simp]

theorem ContinuousLinearMap.opNorm_linearIsometryEquiv_mul {𝕜 : Type u_7} {E : Type u_8} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] (e : E ≃ₗᵢ[𝕜] E) (f : E →L[𝕜] E) : ‖↑↑e * f‖ = ‖f‖

Postcomposition with a linear isometry preserves the operator norm.