Zulip Chat Archive

Stream: general

Topic: cardinal


view this post on Zulip orlando (May 03 2020 at 00:13):

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

view this post on Zulip Kevin Buzzard (May 03 2020 at 00:16):

Is there something like fintype.card_univ?

view this post on Zulip Yury G. Kudryashov (May 03 2020 at 00:22):

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

view this post on Zulip Reid Barton (May 03 2020 at 00:23):

fintype.card_congr $ equiv.set.univ X

view this post on Zulip Kevin Buzzard (May 03 2020 at 00:24):

Would a hammer have found this?

view this post on Zulip Reid Barton (May 03 2020 at 00:24):

I found the second part by library_search

view this post on Zulip Reid Barton (May 03 2020 at 00:25):

Good question though.

view this post on Zulip Kevin Buzzard (May 03 2020 at 00:30):

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.

view this post on Zulip orlando (May 03 2020 at 01:16):

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 !

view this post on Zulip Yury G. Kudryashov (May 03 2020 at 01:22):

One of these should work:

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

view this post on Zulip Yury G. Kudryashov (May 03 2020 at 01:22):

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

view this post on Zulip orlando (May 03 2020 at 02:24):

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:


Last updated: May 14 2021 at 05:20 UTC