Commit 2025-11-04 18:11 d4c295d2

chore: remove redundant measurable space structure on WithLp (#31190) The MeasurableSpace structure over WithLp was introduced globally in [#26249](https://github.com/leanprover-community/mathlib4/pull/26249), so the particular instances that were introduced for NumberField.mixedEmbedding.euclidean.mixedSpace and EuclideanSpace are no longer needed. The measurable space structure on WithLp is not imported in the file where EuclideanSpace.measurableEquiv is defined, so if I want to deprecate EuclideanSpace.measurableEquiv I either have to add a useless import, or deprecate the instances in the file instead of removing them. Thus I did not deprecate it and just removed it.