Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-09-27 17:24 7a4b066c

View on Github →

chore(probability/martingale): use volume_tac in definitions (#16619) Use the tactic volume_tac in the definitions martingale, submartingale, supermartingale, martingale_part and predictable_part. In order to do that, change the order of the arguments of martingale_part and predictable_part.

Estimated changes