Theorems on finite groups, rings, and fields

Stream: new members

[Benjamin]

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]

(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]

(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]

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

[Johan Commelin]

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

[Benjamin]

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]

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]

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]

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

[Kevin Buzzard]

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 $q$ is a splitting field of $X^q-X$ over its prime subfield and we might now have that splitting fields are unique up to (possibly non-unique) isomorphism.

[Benjamin]

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

[Benjamin]

And thanks for the info

[Johan Commelin]

We have the uniqueness of splitting fields

[Johan Commelin]

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