Def MeasureTheory.SignedMeasure.toComplexMeasure

Modification history

2023-05-29 14:32

Mathlib/MeasureTheory/Measure/Complex.lean

feat: port MeasureTheory.Measure.Complex (#4471)

Added MeasureTheory.SignedMeasure.toComplexMeasure View on Github →