Commit 2023-01-10 11:52 ee2b6d9c

View on Github →

feat: port Data.List.Count (#1410)

depends on: #1380

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Data/Bool/Basic.lean

added theorem Bool.beq_comm

added theorem Bool.beq_eq_decide_eq

added theorem Bool.eq_iff_eq_true_iff

Created Mathlib/Data/List/Count.lean

added theorem List.Sublist.count_le

added theorem List.Sublist.countp_le

added theorem List.count_append

added theorem List.count_bind

added theorem List.count_concat

added theorem List.count_cons'

added theorem List.count_cons

added theorem List.count_cons_of_ne

added theorem List.count_cons_self

added theorem List.count_eq_length

added theorem List.count_eq_zero

added theorem List.count_eq_zero_of_not_mem

added theorem List.count_erase

added theorem List.count_erase_of_ne

added theorem List.count_erase_self

added theorem List.count_filter

added theorem List.count_join

added theorem List.count_le_count_cons

added theorem List.count_le_count_map

added theorem List.count_le_length

added theorem List.count_map_of_injective

added theorem List.count_nil

added theorem List.count_pos

added theorem List.count_repeat

added theorem List.count_replicate

added theorem List.count_singleton'

added theorem List.count_singleton

added theorem List.count_tail

added theorem List.countp_append

added theorem List.countp_congr

added theorem List.countp_cons

added theorem List.countp_cons_of_neg

added theorem List.countp_cons_of_pos

added theorem List.countp_eq_length

added theorem List.countp_eq_length_filter

added theorem List.countp_eq_zero

added theorem List.countp_false

added theorem List.countp_filter

added theorem List.countp_join

added theorem List.countp_le_length

added theorem List.countp_map

added theorem List.countp_mono_left

added theorem List.countp_nil

added theorem List.countp_pos

added theorem List.countp_true

added theorem List.le_count_iff_repeat_sublist

added theorem List.le_count_iff_replicate_sublist

added theorem List.length_eq_countp_add_countp

added theorem List.length_filter_lt_length_iff_exists

added theorem List.not_mem_of_count_eq_zero

added theorem List.one_le_count_iff_mem

added theorem List.prod_eq_pow_single

added theorem List.prod_map_eq_pow_single

added theorem List.repeat_count_eq_of_count_eq_length

added theorem List.replicate_count_eq_of_count_eq_length

Modified Mathlib/Logic/Function/Basic.lean

added theorem Function.Injective.beq_eq