Theorem MeasureTheory.Measure.toSphere_eq_zero_iff_finrank

Modification history

2025-09-27 15:46
Mathlib/MeasureTheory/Constructions/HaarToSphere.lean
feat(HaarToSphere): add integrability lemmas (#24248)
Added MeasureTheory.Measure.toSphere_eq_zero_iff_finrankView on Github →