Theorem ProbabilityTheory.Kernel.iIndepFun.comp

Modification history

2025-12-05 16:31

Mathlib/Probability/Independence/Kernel/Indep.lean

chore(Probability): split `Independence.Kernel` (#32327) …

Modified ProbabilityTheory.Kernel.iIndepFun.comp View on Github →

2024-10-16 14:07

Mathlib/Probability/Independence/Kernel.lean

feat: post-composing independent random variables (#17811) …

Added ProbabilityTheory.Kernel.iIndepFun.comp View on Github →