Theorem ProbabilityTheory.Kernel.IsDeterministic.exists_eq_deterministic

Modification history

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