mathlib

652357ac - feat(data/nat/choose/sum): alternate forms of the binomial theorem (#7415)