Commit 2024-01-05 10:17 4d385393

View on Github →

feat: IndepFun.symm of different domains (#9425)

Estimated changes

Modified Mathlib/Probability/Independence/Basic.lean

modified theorem ProbabilityTheory.IndepFun.ae_eq

Modified Mathlib/Probability/Independence/Kernel.lean

modified theorem ProbabilityTheory.kernel.IndepFun.ae_eq