Count

📁 Source: Mathlib/Data/Bool/Count.lean

Statistics

Metric	Count
Definitions	0
Theorems count_not, count_false_eq_count_true, count_false_le_count_true_add_one, count_not_cons, count_not_eq_count, count_not_le_count_add_one, count_true_le_count_false_add_one, length_div_two_le_count_bool, length_sub_one_le_two_mul_count_bool, two_mul_count_bool_eq_ite, two_mul_count_bool_le_length_add_one, two_mul_count_bool_of_even, count_add_count_not, count_false_add_count_true, count_not_add_count, count_true_add_count_false	16
Total	16

List

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
count_add_count_not 📖	—	—	—	—	—
count_false_add_count_true 📖	—	—	—	—	count_not_add_count
count_not_add_count 📖	—	—	—	—	—
count_true_add_count_false 📖	—	—	—	—	count_not_add_count

List.Chain

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
count_not 📖	—	—	—	—	List.IsChain.count_not_cons

List.IsChain

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
count_false_eq_count_true 📖	—	Even	—	—	count_not_eq_count
count_false_le_count_true_add_one 📖	—	—	—	—	count_not_le_count_add_one
count_not_cons 📖	—	—	—	—	Bool.not_ne_self add_assoc Nat.mod_two_add_succ_mod_two Bool.eq_not_iff
count_not_eq_count 📖	—	Even	—	—	Bool.not_ne_self count_not_cons Nat.not_even_iff Nat.even_add_one
count_not_le_count_add_one 📖	—	—	—	—	zero_le Nat.instCanonicallyOrderedAdd Bool.not_ne_self count_not_cons add_assoc
count_true_le_count_false_add_one 📖	—	—	—	—	count_not_le_count_add_one
length_div_two_le_count_bool 📖	—	—	—	—	Nat.instAtLeastTwoHAddOfNat two_pos Nat.instZeroLEOneClass IsOrderedAddMonoid.toAddLeftMono Nat.instIsOrderedAddMonoid tsub_le_iff_right Nat.instOrderedSub length_sub_one_le_two_mul_count_bool
length_sub_one_le_two_mul_count_bool 📖	—	—	—	—	two_mul_count_bool_eq_ite Nat.instOrderedSub IsOrderedAddMonoid.toAddLeftMono Nat.instIsOrderedAddMonoid IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT AddLeftCancelSemigroup.toIsLeftCancelAdd contravariant_lt_of_covariant_le Nat.instCanonicallyOrderedAdd
two_mul_count_bool_eq_ite 📖	mathematical	—	Even Nat.instDecidablePredEven	—	two_mul_count_bool_of_even Even.zero mul_add Distrib.leftDistribClass tail Nat.even_add_one mul_one add_tsub_cancel_right Nat.instOrderedSub IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT AddLeftCancelSemigroup.toIsLeftCancelAdd contravariant_lt_of_covariant_le IsOrderedAddMonoid.toAddLeftMono Nat.instIsOrderedAddMonoid Nat.instCharZero Nat.instAtLeastTwoHAddOfNat MulZeroClass.mul_zero add_zero
two_mul_count_bool_le_length_add_one 📖	—	—	—	—	two_mul_count_bool_eq_ite IsOrderedAddMonoid.toAddLeftMono Nat.instIsOrderedAddMonoid IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT AddLeftCancelSemigroup.toIsLeftCancelAdd contravariant_lt_of_covariant_le Nat.instCanonicallyOrderedAdd Nat.instOrderedSub
two_mul_count_bool_of_even 📖	—	Even	—	—	List.count_not_add_count count_not_eq_count Nat.instAtLeastTwoHAddOfNat two_mul

---

← Back to Index