Lemmas to be Ported to Mathlib

This file gives a centralized location to add lemmas that belong better in general mathlib than in the project itself.

theorem Fintype.sum_inv_card (α : Type u_1) [Fintype α] [Nonempty α] : ∑ x : α, (↑(card α))⁻¹ = 1

@[simp]

theorem vector_eq_nil {α : Type u_1} (xs : List.Vector α 0) : xs = List.Vector.nil

theorem List.injective2_cons {α : Type u_1} : Function.Injective2 cons

theorem Vector.injective2_cons {α : Type u_1} {n : ℕ} : Function.Injective2 List.Vector.cons

theorem Prod.mk.injective2 {α : Type u_1} {β : Type u_2} : Function.Injective2 mk

theorem Function.injective2_swap_iff {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α → β → γ) : Injective2 (swap f) ↔ Injective2 f

@[simp]

theorem Finset.image_const_univ {α : Type u_1} {β : Type u_2} [DecidableEq β] [Fintype α] [Nonempty α] (b : β) : image (fun (x : α) => b) univ = {b}

theorem List.countP_eq_sum_fin_ite {α : Type u_1} (xs : List α) (p : α → Bool) : (∑ i : Fin xs.length, if p xs[i] = true then 1 else 0) = countP p xs

Summing 1 over list indices that satisfy a predicate is just countP applied to p.

theorem List.card_filter_getElem_eq {α : Type u_1} [DecidableEq α] (xs : List α) (x : α) : {i : Fin xs.length | xs[i] = x}.card = count x xs

@[simp]

theorem Vector.getElem_eq_get {α : Type u_1} {n : ℕ} (xs : List.Vector α n) (i : ℕ) (h : i < n) : xs[i] = xs.get ⟨i, h⟩

@[simp]

theorem Finset.sum_boole' {ι : Type u_1} {β : Type u_2} [AddCommMonoid β] (r : β) (p : ι → Prop) [DecidablePred p] (s : Finset ι) : (∑ x ∈ s, if p x then r else 0) = (filter p s).card • r

@[simp]

theorem Finset.count_toList {α : Type u_1} [DecidableEq α] (x : α) (s : Finset α) : List.count x s.toList = if x ∈ s then 1 else 0

theorem BitVec.toFin_bijective (n : ℕ) : Function.Bijective toFin

instance instFintypeBitVec_toMathlib (n : ℕ) : Fintype (BitVec n)

Equations

• instFintypeBitVec_toMathlib n = Fintype.ofBijective (fun (x : Fin (2 ^ n)) => { toFin := x }) ⋯

@[simp]

theorem card_bitVec (n : ℕ) : Fintype.card (BitVec n) = 2 ^ n

@[simp]

theorem BitVec.xor_self_xor {n : ℕ} (x y : BitVec n) : x ^^^ (x ^^^ y) = y

instance instInhabitedSubtypeForallBijective_toMathlib (α : Type) [Inhabited α] : Inhabited { f : α → α // Function.Bijective f }

Equations

• instInhabitedSubtypeForallBijective_toMathlib α = { default := ⟨id, ⋯⟩ }

theorem tsum_option {α : Type u_1} {β : Type u_2} [AddCommMonoid α] [TopologicalSpace α] [ContinuousAdd α] [T2Space α] (f : Option β → α) (hf : Summable (Function.update f none 0)) : ∑' (x : Option β), f x = f none + ∑' (x : β), f (some x)

@[simp]

theorem PMF.monad_pure_eq_pure {α : Type u} (x : α) : Pure.pure x = pure x

@[simp]

theorem PMF.monad_bind_eq_bind {α β : Type u} (p : PMF α) (q : α → PMF β) : p >>= q = p.bind q

@[simp]

theorem List.foldlM_range {m : Type u → Type v} [Monad m] [LawfulMonad m] {s : Type u} (n : ℕ) (f : s → Fin n → m s) (init : s) : foldlM f init (finRange n) = Fin.foldlM n f init

theorem list_mapM_loop_eq {m : Type u → Type v} [Monad m] [LawfulMonad m] {α : Type w} {β : Type u} (xs : List α) (f : α → m β) (ys : List β) : List.mapM.loop f xs ys = (fun (x : List β) => ys.reverse ++ x) <$> List.mapM.loop f xs []