no goals
V : Type ?u.314449
V₁✝ : Type ?u.314452
V₂✝ : Type ?u.314455
V₃ : Type ?u.314458
inst✝⁵ : SeminormedAddCommGroup V
inst✝⁴ : SeminormedAddCommGroup V₁✝
inst✝³ : SeminormedAddCommGroup V₂✝
inst✝² : SeminormedAddCommGroup V₃
f✝ g : NormedAddGroupHom V₁✝ V₂✝
V₁ : Type u_1
V₂ : Type u_2
inst✝¹ : NormedAddCommGroup V₁
inst✝ : NormedAddCommGroup V₂
f : NormedAddGroupHom V₁ V₂
hn : ‖f‖ = 0
x : V₁
⊢ ‖f‖ * ‖x‖ = 0
rw [hn, zero_mul]
no goals
V : Type ?u.314449
V₁✝ : Type ?u.314452
V₂✝ : Type ?u.314455
V₃ : Type ?u.314458
inst✝⁵ : SeminormedAddCommGroup V
inst✝⁴ : SeminormedAddCommGroup V₁✝
inst✝³ : SeminormedAddCommGroup V₂✝
inst✝² : SeminormedAddCommGroup V₃
f✝ g : NormedAddGroupHom V₁✝ V₂✝
V₁ : Type u_1
V₂ : Type u_2
inst✝¹ : NormedAddCommGroup V₁
inst✝ : NormedAddCommGroup V₂
f : NormedAddGroupHom V₁ V₂
hf : f = 0
⊢ ‖f‖ = 0
rw [hf, opNorm_zero]