Theorem ProbabilityTheory.Kernel.copy_comp_apply_prod

Modification history

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