Commit 2023-01-26 08:40 8aef3ee9

View on Github →

feat: Port Data.Bool.Count (#1761)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Data/Bool/Count.lean

added theorem List.Chain'.count_false_eq_count_true

added theorem List.Chain'.count_false_le_count_true_add_one

added theorem List.Chain'.count_not_eq_count

added theorem List.Chain'.count_not_le_count_add_one

added theorem List.Chain'.count_true_le_count_false_add_one

added theorem List.Chain'.length_div_two_le_count_bool

added theorem List.Chain'.length_sub_one_le_two_mul_count_bool

added theorem List.Chain'.two_mul_count_bool_eq_ite

added theorem List.Chain'.two_mul_count_bool_le_length_add_one

added theorem List.Chain'.two_mul_count_bool_of_even

added theorem List.Chain.count_not

added theorem List.count_add_count_not

added theorem List.count_false_add_count_true

added theorem List.count_not_add_count

added theorem List.count_true_add_count_false