Documentation

Mathlib.Data.List.Count

Counting in lists #

This file proves basic properties of List.countP and List.count, which count the number of elements of a list satisfying a predicate and equal to a given element respectively. Their definitions can be found in Std.Data.List.Basic.

theorem List.countP_join {α : Type u_1} (p : αBool) (l : List (List α)) :
theorem List.length_filter_lt_length_iff_exists {α : Type u_1} (p : αBool) (l : List α) :

count #

@[deprecated]
theorem List.count_cons' {α : Type u_1} [DecidableEq α] (a : α) (b : α) (l : List α) :
List.count a (b :: l) = List.count a l + if a = b then 1 else 0
theorem List.count_join {α : Type u_1} [DecidableEq α] (l : List (List α)) (a : α) :
theorem List.count_bind {α : Type u_1} {β : Type u_2} [DecidableEq β] (l : List α) (f : αList β) (x : β) :
@[simp]
theorem List.count_map_of_injective {α : Type u_1} {β : Type u_2} [DecidableEq α] [DecidableEq β] (l : List α) (f : αβ) (hf : Function.Injective f) (x : α) :
theorem List.sum_map_eq_nsmul_single {α : Type u_2} {l : List α} [DecidableEq α] {β : Type u_1} [AddMonoid β] (a : α) (f : αβ) (hf : ∀ (a' : α), a' aa' lf a' = 0) :
theorem List.prod_map_eq_pow_single {α : Type u_2} {l : List α} [DecidableEq α] {β : Type u_1} [Monoid β] (a : α) (f : αβ) (hf : ∀ (a' : α), a' aa' lf a' = 1) :
theorem List.sum_eq_nsmul_single {α : Type u_1} {l : List α} [DecidableEq α] [AddMonoid α] (a : α) (h : ∀ (a' : α), a' aa' la' = 0) :
theorem List.prod_eq_pow_single {α : Type u_1} {l : List α} [DecidableEq α] [Monoid α] (a : α) (h : ∀ (a' : α), a' aa' la' = 1) :