## Stream: new members

### Topic: x / x = 1

#### 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?

#### Mario Carneiro (Feb 08 2021 at 21:06):

Is that nat division?

#### Julian Berman (Feb 08 2021 at 21:07):

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

#### Julian Berman (Feb 08 2021 at 21:07):

do I need some : R's?

#### Mario Carneiro (Feb 08 2021 at 21:07):

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

#### 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

#### 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

#### Julian Berman (Feb 08 2021 at 21:08):

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

#### 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

#### 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