mathlib3

06a655b5 - feat(data/list/to_finsupp): computable finsupp from list (#15161)

feat(data/list/to_finsupp): computable finsupp from list (#15161) via `list.nthd` On the way to computable list-based polynomials Co-authored-by: Yakov Pechersky <ffxen158@gmail.com> Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>