Def MeasureTheory.VectorMeasure.dirac

Modification history

2026-01-26 09:20
Mathlib/MeasureTheory/VectorMeasure/Basic.lean
feat: more basic API on vector measures (#34414) …
Added MeasureTheory.VectorMeasure.diracView on Github →