α : Type u_1
E : Type ?u.2301795
F : Type u_2
G : Type ?u.2301801
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
f : α → F
c : ℝ≥0∞
⊢ c ^ ENNReal.toReal (1 / 1) • snorm f 1 μ = c * snorm f 1 μ
α : Type u_1
E : Type ?u.2301795
F : Type u_2
G : Type ?u.2301801
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
f : α → F
c : ℝ≥0∞
⊢ snorm f 1 (c • μ) = c * snorm f 1 μ
rw [@snorm_smul_measure_of_ne_top _ _ _ μ _ 1 (@ENNReal.coe_ne_top 1) f c]
no goals
α : Type u_1
E : Type ?u.2301795
F : Type u_2
G : Type ?u.2301801
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
f : α → F
c : ℝ≥0∞
⊢ c ^ ENNReal.toReal (1 / 1) • snorm f 1 μ = c * snorm f 1 μ
simp