mathlib

c3762602 - chore(analysis/analytic/isolated_zeros): tidy exists_has_sum_smul_of_apply_eq_zero (#16389)