mathlib
87714908 - chore(probability/martingale): move the optional stopping theorem to its own file (#16464)

Commit

3 years ago

chore(probability/martingale): move the optional stopping theorem to its own file (#16464) The idea is to reserve martingale/basic.lean to really basic API about (sub/super)martingales.

Author

RemyDegenne

Parents

d04db585

mathlib 87714908 - chore(probability/martingale): move the optional stopping theorem to its own file (#16464)

mathlib
87714908 - chore(probability/martingale): move the optional stopping theorem to its own file (#16464)