cardinal

Stream: general

[orlando]

Hello, I have a problem :grinning_face_with_smiling_eyes:

Do you have an idea ?

import data.fintype.basic
example (X : Type)[fintype X][decidable_eq X]  : fintype.card ({x : X | true }) = fintype.card X := begin
    -- I don't understand why i'm always dealing with this kind of thing ???

end

[Kevin Buzzard]

Is there something like fintype.card_univ?

[Yury G. Kudryashov]

1. Open fintype/basic
2. Search for card.

[Reid Barton]

fintype.card_congr $ equiv.set.univ X

[Kevin Buzzard]

Would a hammer have found this?

[Reid Barton]

I found the second part by library_search

[Reid Barton]

Good question though.

[Kevin Buzzard]

After a while you learn how to use a type and you pick up sufficiently many tricks that you can solve problems like this yourself. I think I can solve most trivial-to-mathematician questions about natin Lean now.

[orlando]

thx @Reid Barton !
It's ok ! But I have a problem, i think, in my calculus, card is calculate in a ring R and not in nat ... or i don't know that strange :confused:

Rt : ↑(card ↥{x : G | true}) = ↑(card G)
⊢ ↑(card ↥{x : G | true}) = ↑(card G)    --- not the same ↑  and i don't understand for the moment !

I try to isolate the problem tomorow !

[Yury G. Kudryashov]

One of these should work:

1. rw [fintype.card_congr (equiv.set.univ α)].
2. congr, then exact fintype.card_congr (equiv.set.univ α).

[Yury G. Kudryashov]

(I think that both should work but didn't test)

[orlando]

good : i don't understand why but apply fintype.card_congr, exact equiv.set.univ G, work the other proposition doesn't work in my context !

thx @Yury G. Kudryashov and @Reid Barton and @Kevin Buzzard ... i can sleep now :sweat_smile: