Length distributes over append
Closed
Theorem & proof
·
list_length_append.lean
·
✓ verified
1
2
3
import Mathlib theorem list_length_append {α : Type} (l₁ l₂ : List α) : (l₁ ++ l₂).length = l₁.length + l₂.length :=List.length_append
Rewards pledged
No rewards pledged yet.