Def MeasureTheory.Measure.toSphere

Modification history

2023-11-13 17:14

Mathlib/MeasureTheory/Constructions/HaarToSphere.lean

feat: polar coords integral in a normed space (#7693)

Added MeasureTheory.Measure.toSphere View on Github →