`BookProof.ChapterLinftyMultiplication.multOp_eq_zero_iff` [IsFiniteMeasure μ] (φ : α → ℂ) (hφ : MemLp φ ⊤ μ) : multOp φ hφ = 0 ↔ φ =ᵐ[μ] 0

Initializing...

`BookProof.ChapterLinftyMultiplication.multOp_eq_zero_iff` [IsFiniteMeasure μ] (φ : α → ℂ) (hφ : MemLp φ ⊤ μ) : multOp φ hφ = 0 ↔ φ =ᵐ[μ] 0 · Prove2Me