Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-10-25 01:28 951a60ea

View on Github →

chore(data/list/basic): golf a proof (#9949) Prove list.mem_map directly, get list.exists_of_mem_map and list.mem_map_of_mem as corollaries.

Estimated changes

deleted theorem list.exists_of_mem_map
modified theorem list.pmap_eq_map