Zulip Chat Archive

Stream: new members

Topic: x / x = 1


view this post on Zulip Julian Berman (Feb 08 2021 at 21:06):

What do I need to be able to prove:

example {P : Type} [fintype P] [nonempty P] : fintype.card P / fintype.card P = 1 := sorry

Am I using nonempty incorrectly?

view this post on Zulip Mario Carneiro (Feb 08 2021 at 21:06):

Is that nat division?

view this post on Zulip Julian Berman (Feb 08 2021 at 21:07):

I think so if I understand #check fintype.card telling me it returns a natural

view this post on Zulip Julian Berman (Feb 08 2021 at 21:07):

do I need some : R's?

view this post on Zulip Mario Carneiro (Feb 08 2021 at 21:07):

(by which I mean, it is, but are you sure you want to be using it)

view this post on Zulip Mario Carneiro (Feb 08 2021 at 21:08):

It's true either way, but it might be less useful than you intend, depending on what you are using this for

view this post on Zulip Mario Carneiro (Feb 08 2021 at 21:08):

The proof breaks down into x != 0 -> x / x = 1 and nonempty P -> fintype.card P != 0

view this post on Zulip Julian Berman (Feb 08 2021 at 21:08):

Ah, sorry -- no I want division in R.. sec, pasting my code

view this post on Zulip Mario Carneiro (Feb 08 2021 at 21:09):

In that case, it breaks down into (x:real) != 0 -> x/x = 1, (x:real) = 0 <-> x = 0 and the last thing

view this post on Zulip Julian Berman (Feb 08 2021 at 21:12):

Got it think I follow, thanks! Will give that a shot.


Last updated: May 08 2021 at 09:11 UTC