## Stream: Is there code for X?

### Topic: p divides x-x^p

#### Adam Topaz (Sep 26 2020 at 20:45):

Does mathlib have the following example?

import data.nat.prime
open nat
variable (p : primes)
example {x : ℤ} : (p : ℤ) ∣ (x - x^p) := sorry


#### Adam Topaz (Sep 26 2020 at 20:58):

Yeah the proof would follow easily from this and the fact that zmod p is the quotient of Z by the ideal generated by p, and the fact that the equivalence relation for a principal ideal is given by divisibility of the difference by the generator of the ideal. All of these things are presumably in mathlib, and I was hoping someone put them together into such a lemma.

#### Floris van Doorn (Sep 26 2020 at 21:10):

import field_theory.finite
open nat
variable (p : primes)
example {x : ℤ} : (p : ℤ) ∣ (x - x^p) :=
begin
rw [← int.modeq.modeq_iff_dvd],
show x ^ p ≡ x [ZMOD (p : ℕ)],
rw [← zmod.int_coe_eq_int_coe_iff],
exact_mod_cast zmod.pow_card x, exact p.2
end


#### Adam Topaz (Sep 26 2020 at 21:55):

Nice! I wonder if it makes sense to add an elementary_number_theory file/folder for small facts like this?

#### Floris van Doorn (Sep 26 2020 at 22:04):

That might be good.
However, I'm not sure what the "normal form" of these lemmas should be. If you formulate the lemma slightly differently, the proof becomes a little shorter:

import field_theory.finite
open nat
variables (p : ℕ) [fact p.prime]
example {x : ℤ} : (p : ℤ) ∣ x - x ^ p :=
by { rw [← int.modeq.modeq_iff_dvd, ← zmod.int_coe_eq_int_coe_iff], exact_mod_cast @zmod.pow_card p _ x }


(yes, it's mostly shorter because I put everything on 1 line, but there is also 1-2 fewer steps)

#### Adam Topaz (Sep 26 2020 at 22:07):

I still don't know what is mathlib's preferred way to speak about primes. It seems the [fact p.prime] is more common than using the type primes

#### Floris van Doorn (Sep 26 2020 at 22:14):

I have not done much with primes in mathlib, so I also don't know. A general strategy is to follow the conventions of the lemmas you're using (or the majority of the lemmas, if mathlib is not consistent itself). That also makes them easier to apply.

#### Reid Barton (Sep 26 2020 at 22:45):

The divisibility/zmod/ZMOD stuff seems more difficult than it has to be whenever I have to use it, though that could just be wishful thinking.

Last updated: May 07 2021 at 22:14 UTC