Zulip Chat Archive
Stream: Is there code for X?
Topic: A finite field has at least two elements
Michael Stoll (Apr 12 2022 at 17:59):
I can't find something like
lemma finite_field.two_le_card (F : Type*) [field F] [fintype F] : 2 ≤ fintype.card F := sorry
in the library. Is it just me, or do I need to go via the fact that fintype.card F is a prime power and prime powers are at least 2?
Yaël Dillies (Apr 12 2022 at 18:00):
Is that too hard?
Michael Stoll (Apr 12 2022 at 18:00):
No, but the statement seems to be an obvious candidate...
Michael Stoll (Apr 12 2022 at 18:00):
Perhaps it is easier to use that 0 ≠ 1?
Yaël Dillies (Apr 12 2022 at 18:01):
Michael Stoll (Apr 12 2022 at 18:03):
OK.
Eric Rodriguez (Apr 12 2022 at 18:11):
docs#fintype.one_lt_card_iff_nontrivial
Eric Rodriguez (Apr 12 2022 at 18:12):
oh, I see Yael posted this
Adam Topaz (Apr 12 2022 at 18:29):
All fields should have a [nontrivial F] instance, which gives you two nonequal elements
Adam Topaz (Apr 12 2022 at 18:30):
The two lemmas above can then be used to get the bound on cardinality
Last updated: Dec 20 2023 at 11:08 UTC