Zulip Chat Archive

Stream: new members

Topic: Theorems on finite groups, rings, and fields

Benjamin (Sep 14 2020 at 19:40):

How thorough is Lean's treatment of undergraduate results related to the title? For example, does Lean have Carmichael's improvement to Fermat's little theorem? Or that finite fields of a given size are isomorphic? My mistake if there's an easy way to find this out.

Julian Berman (Sep 14 2020 at 19:45):

(I don't know what Carmichael's improvement is, or the general answer to this, but I've been basically using grep.) -- e.g. the statement of Fermat's Little Theorem looks like it's here: https://github.com/leanprover-community/mathlib/blob/7d88b3147e51435ee1bebbc0ae14958e580827ca/src/field_theory/finite.lean#L303-L306

Julian Berman (Sep 14 2020 at 19:47):

(That same file looks like it's about finite fields in general, and imports ring_equiv so some sort of equivalence looks like it's being proven but I don't see exactly the finite field isomorphism...)

Patrick Massot (Sep 14 2020 at 19:51):

Benjamin, do you know about https://leanprover-community.github.io/mathlib-overview.html?

Johan Commelin (Sep 14 2020 at 19:51):

@Benjamin We don't have Galois theory for finite fields yet. But we're reasonably close.

Benjamin (Sep 14 2020 at 19:52):

Thanks. Carmichael's improvement gives a simple function for the smallest exponent m so that a^m \equiv 1 mod n. Euler showed that m=phi(n) works, but it's not always the smallest.

Benjamin (Sep 14 2020 at 19:52):

Thanks, I looked at that link before, but didn't see the theorems mentioned, so I just wanted to check that I wasn't missing anything.

Patrick Massot (Sep 14 2020 at 19:53):

I'm not saying there mentioned, I'm saying this link if good to know since it's meant to provide starting points to explore such kind of questions.

Kevin Buzzard (Sep 14 2020 at 19:56):

the smallest exponent is a pretty messy function: if n=ipiein=\prod_ip_i^{e_i} and we define t(i)t(i) to be ϕ(piei)\phi(p_i^{e_i}) if pip_i is odd, and half this if pi=2p_i=2 and ei3e_i\geq3, then the smallest exponent is the LCM of the tit_i. "simple function" is not the word that springs to mind...

Kevin Buzzard (Sep 14 2020 at 19:58):

But I doubt we have this and I don't think we have much on finite fields yet, although we have splitting fields and are on the way to Galois theory so it won't be long before finite fields can be treated in a conceptual manner. Every field of size qq is a splitting field of XqXX^q-X over its prime subfield and we might now have that splitting fields are unique up to (possibly non-unique) isomorphism.

Benjamin (Sep 14 2020 at 19:59):

Fair enough, I didn't find the function simple when learning about it! Maybe "easily computable" is a better description than "simple."

Benjamin (Sep 14 2020 at 20:00):

And thanks for the info

Johan Commelin (Sep 14 2020 at 20:07):

We have the uniqueness of splitting fields

Johan Commelin (Sep 14 2020 at 20:08):

I think that someone with a bit of motivation can do the finite fields PR in a short amount of time

Last updated: Dec 20 2023 at 11:08 UTC