Commit 2023-09-06 11:21 906a71a0

View on Github →

feat: List.head_mem (#6801)

Estimated changes

Modified Mathlib/Data/List/Basic.lean

added theorem List.head_mem

added theorem List.surjective_head!

deleted theorem List.surjective_head'

deleted theorem List.surjective_head

added theorem List.surjective_head?