Multiplicative group of integers modulo n

Stream: Is there code for X?

[Simon Hudon]

In mathlib, is there any proof that p^φ(n) is the inverse of p modulo n when p and n are co-prime?

[Johan Commelin]

@Chris Hughes :up: :question:

[Chris Hughes]

import data.zmod.basic data.nat.totient group_theory.order_of_element

local notation `φ` := nat.totient

open fintype finset

instance {n : ℕ+} : fintype (units (zmod n)) :=
fintype.of_equiv _ zmod.units_equiv_coprime.symm

lemma card_units_eq_totient (n : ℕ+) :
  card (units (zmod n)) = φ n :=
calc card (units (zmod n)) = card {x : zmod n // x.1.coprime n} :
  fintype.card_congr zmod.units_equiv_coprime
... = φ n : finset.card_congr
  (λ a _, a.1.1)
  (λ a, by simp [a.1.2, a.2.symm] {contextual := tt})
  (λ _ _ h, by simp [subtype.val_injective.eq_iff, (fin.eq_iff_veq _ _).symm])
  (λ b hb, ⟨⟨⟨b, by finish⟩, nat.coprime.symm (by simp at hb; tauto)⟩, mem_univ _, rfl⟩)

lemma pow_totient {n : ℕ+} (x : units (zmod n)) : x ^ φ n = 1 :=
by rw [← card_units_eq_totient, pow_card_eq_one]

[Johan Commelin]

instance {n : ℕ+} : fintype (units (zmod n)) :=
fintype.of_equiv _ zmod.units_equiv_coprime.symm

Hmm, shouldn't there be an instance that says that units R is a fintype if R is?

[Simon Hudon]

Nice! How do I bring that back into nat?

[Chris Hughes]

This is surprisingly difficult. zmod should take a nat really, pnats are messy to work with.

[Simon Hudon]

What if I keep the reasoning in int and just bring the result back into nat? Basically, I have a nat and I'm implementing a probabilistic test of primality (Fermat's test). All I need is to conclude that the number is not prime.

[Mario Carneiro]

namespace zmod
open nat
def unit_of_coprime {n : ℕ+} (x : ℕ) (h : nat.coprime x n) : units (zmod n) :=
have (x * gcd_a x ↑n : zmod n) = 1,
  by rw [← int.cast_coe_nat, ← int.cast_one, ← int.cast_mul,
      zmod.eq_iff_modeq_int, ← int.coe_nat_one, ← (show nat.gcd _ _ = _, from h)];
    simpa using int.modeq.gcd_a_modeq x n,
⟨x, gcd_a x n, this, by simpa [mul_comm] using this⟩
end zmod

namespace nat
@[simp] theorem totient_zero : φ 0 = 0 := rfl
end nat

lemma pow_totient' {x n : ℕ} (h : nat.coprime x n) : x ^ φ n ≡ 1 [MOD n] :=
begin
  rcases nat.eq_zero_or_pos n with rfl | h₁, {simp},
  let n' : ℕ+ := ⟨n, h₁⟩,
  let x' : units (zmod n') := zmod.unit_of_coprime _ h,
  have := pow_totient x',
  apply (zmod.eq_iff_modeq_nat' h₁).1,
  apply_fun (coe:units (zmod n') → zmod n') at this,
  simpa [show (x':zmod n') = x, from rfl],
end

[Simon Hudon]

Wonderful! Thank you! Do you guys want to PR all that or do you want me to do it?

[Chris Hughes]

I might get round to it tomorrow, but I'd be very happy for you to do it.

[Simon Hudon]

I can do it. What files would you put those in?

[Mario Carneiro]

unit_of_coprime should go immediately before coprime_equiv_unit (it is generalized from that), totient_zero should be right after totient, not sure about the ones Chris wrote, which are in the join of a few theories