Euler's Theorem

Stream: Is there code for X?

[Michael Wahlberg]

Is there a code for Euler's Theorem?

[Michael Wahlberg]

In Lean4

[Reid Barton]

Euler proved a lot of theorems, which do you have in mind?

[Michael Wahlberg]

The one about congruence between a^p and a

[Kevin Buzzard]

That's due to Fermat and yes it will be there. On mobile right now but try searching the API docs for Fermat or Fermat-Euler

[Mario Carneiro]

docs#zmod.pow_card, although I can't find a version for int other than docs#int.modeq.pow_card_sub_one_eq_one

[Reid Barton]

I'm guessing these are not yet ported to mathlib 4.

[Reid Barton]

But it's also probably not very hard to prove by hand from what is in mathlib 4 already

[Eric Wieser]

Indeed, quite a way to go before that's ported: port-status#field_theory/finite/basic

[Michael Wahlberg]

Is there a possibility of considering the numbers as group elements in Z/mod pZ and then using docs#pow_card_eq_one ?

[Riccardo Brasca]

Sure, this is also possible. It really depends on the precise version you prefer.

[Michael Wahlberg]

But how do we convert them into group elements? Or is it in the definition of modZ or modN?

[Riccardo Brasca]

This is what I mean by "it depends on which version you prefer". If your statement is about integers than it's maybe better to stick to integers. I suggest you to write in Lean the exact statement you want, and we can suggest how to prove it.

[Michael Wahlberg]

I want to prove Fermat's little theorem for natural numbers in Lean4.

[Johan Commelin]

Riccardo is suggesting that your write the Lean 4 statement yourself. Then we can help with the proof.

[Alex J. Best]

Michael Wahlberg said:

Is there a possibility of considering the numbers as group elements in Z/mod pZ and then using docs#pow_card_eq_one ?

did you write this docs link yourself? you should just need to write docs4#pow_card_eq_one

[Michael Wahlberg]

Here,

theorem fermat_little_theorem (p : ℕ) (hp : Prime p) (a : ℕ)(h :  Nat.coprime a p )  : a ^ (p-1 ) % p = 1  :=

[Floris van Doorn]

I think you're missing a hypothesis on a

[Michael Wahlberg]

Is there a theorem that asserts that (Z/pZ)^* is a group

[Michael Wahlberg]

Or can I prove something is a group here? How does someone do that?

[Michael Wahlberg]

Floris van Doorn said:

I think you're missing a hypothesis on a

Is it fine now?

[Johan Commelin]

@Michael Wahlberg all of this is completely trivial in Lean 3. And if you wait two or three weeks, it is probably also trivial in Lean 4.

[Kevin Buzzard]

@Michael Wahlberg the units of any ring (and more generally any monoid) is a group in lean