Theorems · Theorem

AList.mk.injEq

∀ {α : Type u} {β : α → Type v} (entries : List (Sigma β)) (nodupKeys : entries.NodupKeys) (entries_1 : List (Sigma β))
  (nodupKeys_1 : entries_1.NodupKeys),
  ({ entries := entries, nodupKeys := nodupKeys } = { entries := entries_1, nodupKeys := nodupKeys_1 }) =
    (entries = entries_1)

Defined in: Mathlib.Data.List.AList
Cited by: 1 results in Mathlib
Foundations: Depth 16 from the axioms · uses propext

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites3

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

AListstatement · cited by 122
List.NodupKeysstatement and proof · cited by 53
AList.mk.injproof · cited by 1

Cited by1

Results whose statement or proof uses this declaration.

AList.mk_cons_eq_insertproof · cited by 1