[Merged by Bors] - feat: if an L^p space is complete, so is its target space unless the measure is zero#39614

sgouezel wants to merge 5 commits into

leanprover-community:masterleanprover-community/mathlib4:masterfrom

sgouezel:SG_completeLpsgouezel/mathlib4:SG_completeLpCopy head branch name to clipboard