Theorem ProbabilityTheory.Kernel.iIndepFun_congr'

Modification history

2025-12-05 16:31

Mathlib/Probability/Independence/Kernel/Indep.lean

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

Modified ProbabilityTheory.Kernel.iIndepFun_congr'View on Github →

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 →