no goals
𝕜 : Type u_1
𝕜₂ : Type u_2
𝕜₃ : Type ?u.2592188
E : Type u_3
Eₗ : Type ?u.2592194
F : Type u_4
Fₗ : Type ?u.2592200
G : Type ?u.2592203
Gₗ : Type ?u.2592206
𝓕 : Type ?u.2592209
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedAddCommGroup F
inst✝⁹ : NormedAddCommGroup G
inst✝⁸ : NormedAddCommGroup Fₗ
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : NontriviallyNormedField 𝕜₂
inst✝⁵ : NontriviallyNormedField 𝕜₃
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedSpace 𝕜₂ F
inst✝² : NormedSpace 𝕜₃ G
inst✝¹ : NormedSpace 𝕜 Fₗ
c : 𝕜
σ₁₂ : 𝕜 →+* 𝕜₂
σ₂₃ : 𝕜₂ →+* 𝕜₃
f g : E →SL[σ₁₂] F
x✝ y z : E
inst✝ : RingHomIsometric σ₁₂
hn : ‖f‖ = 0
x : E
⊢ ‖f‖ * ‖x‖ = 0
rw [hn, MulZeroClass.zero_mul]
𝕜 : Type u_1
𝕜₂ : Type u_2
𝕜₃ : Type ?u.2592188
E : Type u_3
Eₗ : Type ?u.2592194
F : Type u_4
Fₗ : Type ?u.2592200
G : Type ?u.2592203
Gₗ : Type ?u.2592206
𝓕 : Type ?u.2592209
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedAddCommGroup F
inst✝⁹ : NormedAddCommGroup G
inst✝⁸ : NormedAddCommGroup Fₗ
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : NontriviallyNormedField 𝕜₂
inst✝⁵ : NontriviallyNormedField 𝕜₃
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedSpace 𝕜₂ F
inst✝² : NormedSpace 𝕜₃ G
inst✝¹ : NormedSpace 𝕜 Fₗ
c : 𝕜
σ₁₂ : 𝕜 →+* 𝕜₂
σ₂₃ : 𝕜₂ →+* 𝕜₃
g : E →SL[σ₁₂] F
x y z : E
inst✝ : RingHomIsometric σ₁₂
⊢ ‖0‖ = 0
𝕜 : Type u_1
𝕜₂ : Type u_2
𝕜₃ : Type ?u.2592188
E : Type u_3
Eₗ : Type ?u.2592194
F : Type u_4
Fₗ : Type ?u.2592200
G : Type ?u.2592203
Gₗ : Type ?u.2592206
𝓕 : Type ?u.2592209
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedAddCommGroup F
inst✝⁹ : NormedAddCommGroup G
inst✝⁸ : NormedAddCommGroup Fₗ
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : NontriviallyNormedField 𝕜₂
inst✝⁵ : NontriviallyNormedField 𝕜₃
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedSpace 𝕜₂ F
inst✝² : NormedSpace 𝕜₃ G
inst✝¹ : NormedSpace 𝕜 Fₗ
c : 𝕜
σ₁₂ : 𝕜 →+* 𝕜₂
σ₂₃ : 𝕜₂ →+* 𝕜₃
f g : E →SL[σ₁₂] F
x y z : E
inst✝ : RingHomIsometric σ₁₂
⊢ f = 0 → ‖f‖ = 0
rintro rfl
no goals
𝕜 : Type u_1
𝕜₂ : Type u_2
𝕜₃ : Type ?u.2592188
E : Type u_3
Eₗ : Type ?u.2592194
F : Type u_4
Fₗ : Type ?u.2592200
G : Type ?u.2592203
Gₗ : Type ?u.2592206
𝓕 : Type ?u.2592209
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedAddCommGroup F
inst✝⁹ : NormedAddCommGroup G
inst✝⁸ : NormedAddCommGroup Fₗ
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : NontriviallyNormedField 𝕜₂
inst✝⁵ : NontriviallyNormedField 𝕜₃
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedSpace 𝕜₂ F
inst✝² : NormedSpace 𝕜₃ G
inst✝¹ : NormedSpace 𝕜 Fₗ
c : 𝕜
σ₁₂ : 𝕜 →+* 𝕜₂
σ₂₃ : 𝕜₂ →+* 𝕜₃
g : E →SL[σ₁₂] F
x y z : E
inst✝ : RingHomIsometric σ₁₂
⊢ ‖0‖ = 0
exact op_norm_zero