Cardinality of the type of linear orders on a fintype

Stream: Is there code for X?

[Sophie Morel]

I am using the fact that the cardinality of the type of linear orders on a Fintype V is the factorial of Fintype.card V. Is this or a related statement somewhere in mathlib ?
To be totally honest, I only really need the statement when Fintype.card V is equal to 2, so of course I can just easily prove it by hand, but (1) yuck and (2) I am curious.

[Yaël Dillies]

Yes, but it is stated in terms of docs#equiv.perm: docs#fintype.card_perm

[Sophie Morel]

Yaël Dillies said:

Yes, but it is stated in terms of docs#equiv.perm: docs#fintype.card_perm

Thanks ! Hmm, that's what I feared, I would still have to prove the equivalence between linear orders on a fintype and permutations... I think that I am going to count by hand in my particular case, as I already did in the Lean3 version.

[Sophie Morel]

Well, we'll see... I think that I found all the necessary lemmas about finite ordinals to prove the more general statement less suffering than expected, so now I am tempted. :big_smile:

[Yaël Dillies]

I have the transitive action of perm α on linear_order α and its faithfulness when α is finite, which is enough to get the equivalence. I needed those to formalise the Alon proof of Turán.

[Yaël Dillies]

However, it's exam season, so ask me again in 10 days...

[Sophie Morel]

Yaël Dillies said:

However, it's exam season, so ask me again in 10 days...

Okay, I am starring this message so I don't forget.