Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
feat(data/list/basic): add lemma map_eq_repeat_iff (#17832)
This small PR adds the following API lemma for lists: ```lean lemma map_eq_repeat_iff {α β} {l : list α} {f : α → β} {b : β} : l.map f = repeat b l.length ↔ (∀ x ∈ l, f x = b) ``` See this [Zulip thread](https://leanprover.zulipchat.com/#narrow/stream/217875-Is-there-code-for-X.3F/topic/More.20general.20version.20of.20.60list.2Emap_const.60.3F/near/314118320). (It also fixes a harmless typo in the proof of `last_map`.)
- Loading branch information