Mathlib v3 is deprecated. Go to Mathlib v4

Theorem nonempty_sum

Modification history

2021-12-15 19:58

src/logic/basic.lean

split(logic/nonempty): Split off `logic.basic` (#10762) …

Modified nonempty_sum View on Github →

2017-12-14 21:29

logic/basic.lean

feat(logic/basic): add rewrite rules for nonempty

Added nonempty_sum View on Github →