Theorem Finset.abs_sum_of_nonneg'

Modification history

2023-08-10 19:52

Mathlib/Algebra/BigOperators/Order.lean

chore: banish `Type _` and `Sort _` (#6499) …

Modified Finset.abs_sum_of_nonneg'View on Github →

2023-01-20 09:47

Mathlib/Algebra/BigOperators/Order.lean

feat: port Algebra.BigOperators.Order (#1673)

Added Finset.abs_sum_of_nonneg'View on Github →