Theorem ProbabilityTheory.Kernel.iIndepFun_precomp_of_bijective

Modification history

2025-12-05 16:31
Mathlib/Probability/Independence/Kernel/Indep.lean
chore(Probability): split `Independence.Kernel` (#32327) …
Modified ProbabilityTheory.Kernel.iIndepFun_precomp_of_bijectiveView on Github →
2025-11-24 14:10
Mathlib/Probability/Independence/Kernel.lean
feat(Probability/Independence): reindexing lemmas for `iIndep*` (#31309)
Added ProbabilityTheory.Kernel.iIndepFun_precomp_of_bijectiveView on Github →