mathlib

0f06bccf - feat(data/list/{basic,join}): towards `take_join` (#17190)

feat(data/list/{basic,join}): towards `take_join` (#17190) Co-authored-by: Patrick Johnson <reflexivetransitiveclosure@gmail.com> Co-authored-by: madvorak <dvorakmartinbridge@seznam.cz> Co-authored-by: Martin Dvořák <dvorakmartinbridge@seznam.cz>