mathlib3

24013e2b - feat(data/finsupp/basic): add finsupp.single_left_injective and docstrings (#7207)