Commit 2024-10-21 07:59 797cd917

View on Github →

chore(ConditionalProbability): review argument implicitness (#17910) Make the proof arguments come first and make the measure argument implicit when it can be inferred from the later arguments

Estimated changes

Modified Archive/Wiedijk100Theorems/BallotProblem.lean

Modified Mathlib/Probability/ConditionalProbability.lean

modified theorem ProbabilityTheory.cond_add_cond_compl_eq

modified theorem ProbabilityTheory.cond_apply'

modified theorem ProbabilityTheory.cond_apply

modified theorem ProbabilityTheory.cond_cond_eq_cond_inter

modified theorem ProbabilityTheory.cond_empty

modified theorem ProbabilityTheory.cond_eq_inv_mul_cond_mul

modified theorem ProbabilityTheory.cond_inter_self

modified theorem ProbabilityTheory.cond_mul_eq_inter

modified theorem ProbabilityTheory.cond_pos_of_inter_ne_zero

modified theorem ProbabilityTheory.cond_univ

Modified Mathlib/Probability/UniformOn.lean