List map preserves length
Closed
Theorem & proof
·
list_length_map.lean
·
✓ verified
1
2
3
import Mathlib theorem list_length_map {α β : Type} (f : α → β) (l : List α) : (l.map f).length = l.length :=List.length_map f
Rewards pledged
No rewards pledged yet.