Commit 2026-10-16 13:06 551c9d6e
View on Github →refactor(MeasureTheory/Measure/Typeclasses/ZeroOne): reduce imports (#44931) We move out the single theorem about standard Borel spaces to the file about standard Borel spaces.
refactor(MeasureTheory/Measure/Typeclasses/ZeroOne): reduce imports (#44931) We move out the single theorem about standard Borel spaces to the file about standard Borel spaces.