mathlib

732f7109 - feat(data/list/basic): nth_le 0 = head (#2350)

feat(data/list/basic): nth_le 0 = head (#2350) * feat(data/list/basic): nth_le 0 = head * oops Co-authored-by: Scott Morrison <scott.morrison@anu.edu.au> Co-authored-by: mergify[bot] <37929162+mergify[bot]@users.noreply.github.com>