Theorem List.head?_flatten_replicate

Modification history

2025-03-05 13:18
Mathlib/Data/List/Basic.lean
feat(Data/List/Basic): add `head?_flatten_replicate`/`getLast?_flatten_replicate` (#22510) …
Added List.head?_flatten_replicateView on Github →