Mathlib v3 is deprecated. Go to Mathlib v4

Theorem alist.insert_rec_insert

Modification history

2023-01-20 00:18

src/data/list/alist.lean

feat(data/list/alist): recursion on `alist` using `insert` (#15434)

Added alist.insert_rec_insert View on Github →