# Zulip Chat Archive

## 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, `pnat`

s 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