α : Type u_1
E : Type u_2
F : Type ?u.407281
G : Type ?u.407284
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
⊢ ENNReal.toNNReal (snorm (↑↑0) p μ) = 0
α : Type u_1
E : Type u_2
F : Type ?u.407281
G : Type ?u.407284
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
⊢ ‖0‖₊ = 0
rw [nnnorm_def]
α : Type u_1
E : Type u_2
F : Type ?u.407281
G : Type ?u.407284
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
⊢ ENNReal.toNNReal (snorm (↑0) p μ) = 0
α : Type u_1
E : Type u_2
F : Type ?u.407281
G : Type ?u.407284
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
⊢ ENNReal.toNNReal (snorm (↑↑0) p μ) = 0
change (snorm (⇑(0 : α →ₘ[μ] E)) p μ).toNNReal = 0
no goals
α : Type u_1
E : Type u_2
F : Type ?u.407281
G : Type ?u.407284
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
⊢ ENNReal.toNNReal (snorm (↑0) p μ) = 0
simp [snorm_congr_ae AEEqFun.coeFn_zero, snorm_zero]