Commit 2025-11-02 17:39 fb20ff93

View on Github →

chore: fix typo in IndepSets.bUnion (#31181)

Estimated changes

Modified Mathlib/Probability/Independence/Basic.lean

deleted theorem ProbabilityTheory.IndepSets.bUnion

added theorem ProbabilityTheory.IndepSets.biUnion

Modified Mathlib/Probability/Independence/Conditional.lean

deleted theorem ProbabilityTheory.CondIndepSets.bUnion

added theorem ProbabilityTheory.CondIndepSets.biUnion

Modified Mathlib/Probability/Independence/Kernel.lean

deleted theorem ProbabilityTheory.Kernel.IndepSets.bUnion

added theorem ProbabilityTheory.Kernel.IndepSets.biUnion