New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

card s = 1 ↔ ∃ a, s = a::0 #200

Closed

kbuzzard wants to merge 1 commit into leanprover-community:master from kbuzzard:multiset_singleton

Member

kbuzzard commented Jul 16, 2018

I need it, my proof seems to be about twice as long as all the other proofs around it -- do you want it?


          card s = 1 ↔ ∃ a, s = a::0

dd99765

digama0 added a commit that referenced this pull request


          feat(data/multiset,...): card_eq_one

631207b

based on #200

Member

digama0 commented Jul 16, 2018

added in 631207b

digama0 closed this

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment