p divides x-x^p

Stream: Is there code for X?

[Adam Topaz]

Does mathlib have the following example?

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

[Heather Macbeth]

docs#zmod.pow_card ?

[Adam Topaz]

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]

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]

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

[Floris van Doorn]

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]

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]

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]

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.