Theorem ProbabilityTheory.Kernel.isDeterministic_iff_isZeroOneMeasure

Modification history

2026-05-04 16:33
Mathlib/Probability/Kernel/Deterministic.lean
feat(Probability/Kernel): define `IsDeterministic` (#38211) …
Added ProbabilityTheory.Kernel.isDeterministic_iff_isZeroOneMeasureView on Github →