Theorem ProbabilityTheory.Kernel.iIndepFun_congr'

Modification history

2025-08-03 18:35
Mathlib/Probability/Independence/Kernel.lean
feat: random variables are independent iff their joint distribution is the product measure (#26265) …
Added ProbabilityTheory.Kernel.iIndepFun_congr'View on Github →