mathlib

616e6ef3 - feat(data/sign): Allocating signs (#14335)

feat(data/sign): Allocating signs (#14335) A sum of integers of absolute value less than `n` can be broken up as a sum of less than `n` signs.