Commit 2025-10-21 14:19 2c2e8568
View on Github →feat: remove unnecessary nonempty assumption at expect lemmas (#30502)
feat: Dropped unnecessary Nonempty assumptions in
expect_eq_zero_iff_of_nonpos and expect_eq_zero_iff_of_nonneg
(the Finset and Fintype versions)