## Stream: Is there code for X?

### Topic: Multiplicative group of integers modulo n

#### Simon Hudon (Mar 14 2020 at 19:38):

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 (Mar 14 2020 at 19:41):

@Chris Hughes :up: :question:

#### Chris Hughes (Mar 14 2020 at 20:00):

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 (Mar 14 2020 at 20:15):

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 (Mar 14 2020 at 20:23):

Nice! How do I bring that back into nat?

#### Chris Hughes (Mar 14 2020 at 20:31):

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

#### Simon Hudon (Mar 14 2020 at 20:34):

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 (Mar 15 2020 at 00:30):

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 (Mar 15 2020 at 01:19):

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

#### Chris Hughes (Mar 15 2020 at 01:25):

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

#### Simon Hudon (Mar 15 2020 at 02:26):

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

#### Mario Carneiro (Mar 15 2020 at 02:54):

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

Last updated: May 07 2021 at 19:12 UTC