Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2023-01-14 17:40 761f9170

View on Github →

chore(archive/100-theorems-list/30_ballot_problem): golf (#18126) Also add some supporting lemmas.

Estimated changes

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

added theorem ballot.counted_eq_nil_iff

modified theorem ballot.counted_ne_nil_right

modified theorem ballot.length_of_mem_counted_sequence

added theorem ballot.mem_counted_sequence_iff_perm

modified theorem ballot.mem_of_mem_counted_sequence

modified theorem ballot.sum_of_mem_counted_sequence

Modified src/data/list/basic.lean

Modified src/data/list/perm.lean

added theorem list.perm.subset_congr_left

added theorem list.perm.subset_congr_right

added theorem list.perm_repeat_append_repeat

Modified src/logic/basic.lean

added theorem decidable.and_forall_ne