-
Notifications
You must be signed in to change notification settings - Fork 312
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
feat(Probability/BorelCantelli): clarify documentation (#8527)
Some of the students from my Lean seminar got quite confused trying to find the Borel-Cantelli lemmas in Mathlib, because there is a file `Probability.Martingale.BorelCantelli` but neither of the Borel-Cantelli lemmas are in it! This PR adds cross-links between the documentation strings for the various files concerned. (There are no changes to actual code.)
- Loading branch information
Showing
3 changed files
with
13 additions
and
3 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters