Theorem MeasureTheory.Measure.toSphere_apply'

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_apply'View on Github →