mathlib

d61f638a - chore(data/finsupp/defs): redefine `finsupp.single` as `pi.single` (#17356)

chore(data/finsupp/defs): redefine `finsupp.single` as `pi.single` (#17356) This also brings it in line with `dfinsupp.single`. Note that the two are still not defeq due to different decidability instances, but things are least more consistent now. In order to make some proofs still unify, this makes some type arguments explicit to `constant_coeff_C` and `constant_coeff_X`. These lemmas should have had these as explicit arguments anyway, as the type can't be inferred from the other arguments.