Add Topic: Probability

[LorenzoLuccioli]

Add the file Topics.Probability with some simple exercises about probability theory, independence of sets, definition of conditional probability and Bayes' theorem.

• depends on: Bump Mathlib and Lean #12

[RemyDegenne]

You should also add the file to the list of topics files at the bottom of 03Forall.lean (in both exercises and solutions).

[pitmonticone]

There are a few minor typos. You can directly commit the suggested changes.

[pitmonticone]

Now it looks good to me.

Thank you @LorenzoLuccioli for the PR and @RemyDegenne for the review comment!

[fpvandoorn]

For future reference: the script mk_exercises.py generates the exercise files from the solution files (if the solution file is properly marked with -- sorry comments)

[fpvandoorn]

The new probability file should probably get -- sorry commands so that the script also works for it.

[PatrickMassot]

Thanks! Indeed it needs to be adapted to work with mk_exercises.

[pitmonticone]

@LorenzoLuccioli You just need to commit the suggested changes and run:

python3 mk_exercises.py

[pitmonticone]

Ok, now it looks good to me.

Thank you again @LorenzoLuccioli!