Commit 2024-10-11 07:20 3390e404

View on Github →

chore: rename condCount to uniformOn (#17571)

Estimated changes

Modified Archive/Wiedijk100Theorems/BallotProblem.lean

modified theorem Ballot.ballot_edge

modified theorem Ballot.ballot_same

Modified Archive/Wiedijk100Theorems/BirthdayProblem.lean

Modified Mathlib.lean

Deleted Mathlib/Probability/CondCount.lean

deleted def ProbabilityTheory.condCount

deleted theorem ProbabilityTheory.condCount_add_compl_eq

deleted theorem ProbabilityTheory.condCount_compl

deleted theorem ProbabilityTheory.condCount_disjoint_union

deleted theorem ProbabilityTheory.condCount_empty

deleted theorem ProbabilityTheory.condCount_empty_meas

deleted theorem ProbabilityTheory.condCount_eq_one_of

deleted theorem ProbabilityTheory.condCount_eq_zero_iff

deleted theorem ProbabilityTheory.condCount_inter'

deleted theorem ProbabilityTheory.condCount_inter

deleted theorem ProbabilityTheory.condCount_inter_self

deleted theorem ProbabilityTheory.condCount_isProbabilityMeasure

deleted theorem ProbabilityTheory.condCount_of_univ

deleted theorem ProbabilityTheory.condCount_self

deleted theorem ProbabilityTheory.condCount_singleton

deleted theorem ProbabilityTheory.condCount_union

deleted theorem ProbabilityTheory.condCount_univ

deleted theorem ProbabilityTheory.finite_of_condCount_ne_zero

deleted theorem ProbabilityTheory.pred_true_of_condCount_eq_one

Created Mathlib/Probability/UniformOn.lean

added theorem ProbabilityTheory.finite_of_uniformOn_ne_zero

added theorem ProbabilityTheory.pred_true_of_uniformOn_eq_one

added def ProbabilityTheory.uniformOn

added theorem ProbabilityTheory.uniformOn_add_compl_eq

added theorem ProbabilityTheory.uniformOn_compl

added theorem ProbabilityTheory.uniformOn_disjoint_union

added theorem ProbabilityTheory.uniformOn_empty

added theorem ProbabilityTheory.uniformOn_empty_meas

added theorem ProbabilityTheory.uniformOn_eq_one_of

added theorem ProbabilityTheory.uniformOn_eq_zero_iff

added theorem ProbabilityTheory.uniformOn_inter'

added theorem ProbabilityTheory.uniformOn_inter

added theorem ProbabilityTheory.uniformOn_inter_self

added theorem ProbabilityTheory.uniformOn_isProbabilityMeasure

added theorem ProbabilityTheory.uniformOn_of_univ

added theorem ProbabilityTheory.uniformOn_self

added theorem ProbabilityTheory.uniformOn_singleton

added theorem ProbabilityTheory.uniformOn_union

added theorem ProbabilityTheory.uniformOn_univ

Modified scripts/no_lints_prime_decls.txt