mathlib3
7a4b066c - chore(probability/martingale): use volume_tac in definitions (#16619)

Commit
3 years ago
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`.
Author
Parents
Loading