mathlib

57345aed - feat (data/sign): `sign_sum` (#17657)

feat (data/sign): `sign_sum` (#17657) Add the lemma that, if all the terms in a nonempty sum (in a `linear_ordered_add_comm_group`) have the same sign, the sum has that sign.