Theorem ProbabilityTheory.Kernel.iIndepFun.indepFun_mul_right₀

Modification history

2025-12-05 16:31
Mathlib/Probability/Independence/Kernel/Indep.lean
chore(Probability): split `Independence.Kernel` (#32327) …
Modified ProbabilityTheory.Kernel.iIndepFun.indepFun_mul_right₀View on Github →
2025-03-23 16:04
Mathlib/Probability/Independence/Kernel.lean
feat: remove measurable assumptions in Azuma-Hoeffding inequality (#23070)
Added ProbabilityTheory.Kernel.iIndepFun.indepFun_mul_right₀View on Github →