`BookProof.ChapterLinftyMaximalAbelian.oneLp_coeFn` : (oneLp μ : α → ℂ) =ᵐ[μ] fun _ => (1 : ℂ)

Initializing...

`BookProof.ChapterLinftyMaximalAbelian.oneLp_coeFn` : (oneLp μ : α → ℂ) =ᵐ[μ] fun _ => (1 : ℂ) · Prove2Me