Theorem MeasureTheory.Measure.toSphere_apply_univ'

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