Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2023-05-11 07:22 2f834701

View on Github →

chore(probability/independence): create independence folder, split old file into two parts (#18987) Split probability/independence into two files, to put Kolmogorov's zero-one law in its own file. The two new files are placed in an independence folder. Also fix a typo in a name in probability/borel_cantelli.

Estimated changes