Theorem ProbabilityTheory.iIndepFun.congr

Modification history

2025-08-03 18:35
Mathlib/Probability/Independence/Basic.lean
feat: random variables are independent iff their joint distribution is the product measure (#26265) …
Deleted ProbabilityTheory.iIndepFun.congrView on Github →
2025-03-23 16:04
Mathlib/Probability/Independence/Basic.lean
feat: remove measurable assumptions in Azuma-Hoeffding inequality (#23070)
Added ProbabilityTheory.iIndepFun.congrView on Github →