mathlib

1f476e67 - feat(data/sum/basic): add basic lemmas (#17059)