Zulip Chat Archive

Stream: Is there code for X?

Topic: Multiplicative group of integers modulo n


view this post on Zulip 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?

view this post on Zulip Johan Commelin (Mar 14 2020 at 19:41):

@Chris Hughes :up: :question:

view this post on Zulip 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]

view this post on Zulip 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?

view this post on Zulip Simon Hudon (Mar 14 2020 at 20:23):

Nice! How do I bring that back into nat?

view this post on Zulip Chris Hughes (Mar 14 2020 at 20:31):

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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip Simon Hudon (Mar 15 2020 at 02:26):

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

view this post on Zulip 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