## Stream: new members

### Topic: Modular arithmetic

#### Nerya (Jan 03 2021 at 14:52):

hello,
in the last few weeks i have learnd lean and now i want to start proving thing in Modular arithmetic up to Chinese remainder theorem, and hopefully to prove the whole rsa system, is there any libraries already written about that?
thank you very much

#### Kenny Lau (Jan 03 2021 at 14:57):

well we have the ring-theoretic version of the Chinese Remainder Theorem (written by yours truly!) if that helps

#### Kevin Buzzard (Jan 03 2021 at 15:51):

Of course that doesn't stop you proving it again, especially if you want some practice :-) I would recommend working with integers rather than naturals.

#### Adam Topaz (Jan 03 2021 at 16:11):

Since you mention RSA, you might be interested in docs#nat.modeq.pow_totient

#### Adam Topaz (Jan 03 2021 at 16:13):

I'm sure we also have the multiplicativity of the totient function, but I can't find it right now...

#### Kevin Buzzard (Jan 03 2021 at 16:13):

Perhaps a place to start is that totient is multiplicative? Do we have that? I can't immediately spot it. How will one prove $\phi(pq)=(p-1)(q-1)$?

#### Adam Topaz (Jan 03 2021 at 16:14):

Ok maybe I'm not so sure :wink:

#### Nerya (Jan 03 2021 at 16:15):

wow i can see you done a lot of fine work already, lets see if i can find myself in there

#### Kevin Buzzard (Jan 03 2021 at 16:15):

The maths proof would be to prove $\phi(n)=|(\mathbb{Z}/n\mathbb{Z})^\times|$ and to use ring CRT

#### Adam Topaz (Jan 03 2021 at 16:27):

Oh yeah this should be easy since we have CRT and docs#zmod.card_units_eq_totient

#### Shing Tak Lam (Jan 03 2021 at 16:39):

Is docs#nat.modeq.chinese_remainder the nat version of CRT? Looks like it to me.

#### Adam Topaz (Jan 03 2021 at 16:42):

This is the actual theorem
docs#nat.modeq.modeq_and_modeq_iff_modeq_mul

#### Adam Topaz (Jan 03 2021 at 16:45):

But you need the statements about the cardinality of units for the multiplicativity of totient, and I think it would be annoying to use this version to prove that

#### Arcayn (Jan 04 2021 at 12:39):

This is really spooky as I haven't seen this but just proved RSA over the weekend

#### Arcayn (Jan 04 2021 at 12:40):

I needed to prove multiplicativity for it plus values on prime inputs, I will potentially PR it although the naive number-theoretic approach is possibly less valuable than using the ring theortic version of the CRT

#### Kevin Buzzard (Jan 04 2021 at 12:45):

What exactly did you prove? PS I assume you're the person who told me they'd done this on the Discord earlier ;-)

#### Arcayn (Jan 04 2021 at 12:56):

Yes I am ! let me just post the theorem statement here - I imagine you could make a more powerful version which doesn't require the private key d to be provided but I didn't really want to mess around with switching between nat and zmod to find modular inverses etc. at the moment as I'm still fairly new :)

theorem rsa_is_correct {p q m e d : } (h_e : e  1)  (h_p : p.prime) (h_q : q.prime) (p_neq_q : p  q) (h_1 : (p * q).totient.modeq (e * d) 1) :
(p * q).modeq ((m ^ e) ^ d) m

#### Arcayn (Jan 04 2021 at 12:59):

And just for the sake of completeness

lemma mul_totient {a b : } (h : a.coprime b) : (a * b).totient = a.totient * b.totient

#### Kevin Buzzard (Jan 04 2021 at 13:04):

Nice! These, and also evaluation of totient function on prime powers, would surely be welcome additions to mathlib.

#### Arcayn (Jan 04 2021 at 13:05):

(note that this is the version of the proof that does not require m to be coprime to n and doesn't invoke nat.modeq.pow_totient but instead zmod.units_pow_card_sub_one_eq_one. If we base this proof on Euler's theorem, afaik we would not need multiplicativity of phi)

#### Arcayn (Jan 04 2021 at 13:06):

Yes, I also proved

lemma prime_totient {a : } (h : a.prime) : a.totient = a - 1

Which is trivially extensible to prime powers i think

#### Eric Wieser (Jan 04 2021 at 13:12):

It sounds like you should be able to redefine totient as an arithmetic_function, and provide totient_is_multiplicative : totient.is_multiplicative

Last updated: May 10 2021 at 00:31 UTC