mathlib
c8961621 - feat(data/finset/basic) eq_of_mem_singleton (#10414)

Commit
4 years ago
feat(data/finset/basic) eq_of_mem_singleton (#10414) The `finset` equivalent of [set.eq_of_mem_singleton](https://leanprover-community.github.io/mathlib_docs/find/set.eq_of_mem_singleton/src) Co-authored-by: Iván Sadofschi Costa <isadofschi@users.noreply.github.com>
Author
Parents
Loading