no goals
α : Type u_1
E : Type ?u.1108617
F : Type u_2
G : Type ?u.1108623
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedAddCommGroup G
c : F
hq_pos : 0 < q
inst✝ : IsProbabilityMeasure μ
⊢ snorm' (fun x => c) q μ = ↑‖c‖₊
simp [snorm'_const c hq_pos, measure_univ]