Mathlib Changelog
v4
Changelog
About
Github
Commit
2023-11-17 11:02
414c0c82
View on Github →
feat: Add Set.Nonempty.eq_zero and variations (
#8423
) See
the Zulip thread
Estimated changes
Modified
Mathlib/Data/Set/Basic.lean
added
theorem
Set.Nonempty.eq_one
added
theorem
Set.Nonempty.eq_zero
added
theorem
Set.eq_of_nonempty_of_subsingleton'
added
theorem
Set.eq_of_nonempty_of_subsingleton