mathlib3

b685f506 - feat(data/finset/pointwise): `a • (s ∩ t) = a • s ∩ a • t` (#18682)

feat(data/finset/pointwise): `a • (s ∩ t) = a • s ∩ a • t` (#18682) I added the corresponding `set` lemmas a while back, but forgot about their `finset` counterpart. Also additivise `finset.is_central_scalar`/`set.is_central_scalar`.