Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-06-09 13:27 dfc54a3a

View on Github →

feat(combinatorics/ballot): the Ballot problem (#13592)

Estimated changes

Created archive/100-theorems-list/30_ballot_problem.lean

added theorem ballot.ballot_edge

added theorem ballot.ballot_neg

added theorem ballot.ballot_pos

added theorem ballot.ballot_problem'

added theorem ballot.ballot_problem

added theorem ballot.ballot_same

added theorem ballot.count_counted_sequence

added theorem ballot.counted_left_zero

added theorem ballot.counted_ne_nil_left

added theorem ballot.counted_ne_nil_right

added theorem ballot.counted_right_zero

added def ballot.counted_sequence

added theorem ballot.counted_sequence_finite

added theorem ballot.counted_sequence_int_neg_counted_succ_succ

added theorem ballot.counted_sequence_int_pos_counted_succ_succ

added theorem ballot.counted_sequence_nonempty

added theorem ballot.counted_succ_succ

added theorem ballot.disjoint_bits

added theorem ballot.first_vote_neg

added theorem ballot.first_vote_pos

added theorem ballot.head_mem_of_nonempty

added theorem ballot.length_of_mem_counted_sequence

added theorem ballot.mem_of_mem_counted_sequence

added def ballot.stays_positive

added theorem ballot.stays_positive_cons_pos

added theorem ballot.stays_positive_nil

added theorem ballot.sum_of_mem_counted_sequence

Modified docs/100.yaml

Modified src/data/list/infix.lean

added theorem list.mem_of_mem_suffix

Modified src/data/nat/basic.lean

added theorem nat.diag_induction

Modified src/data/real/ennreal.lean

added theorem ennreal.div_eq_div_iff

added theorem ennreal.eq_div_iff

Modified src/measure_theory/measure/measure_space.lean

added theorem measure_theory.measure.count_injective_image

Modified src/probability/cond_count.lean

modified theorem probability_theory.cond_count_add_compl_eq

modified theorem probability_theory.cond_count_compl