Zulip Chat Archive

Stream: new members

Topic: Modular arithmetic


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

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

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

view this post on Zulip Adam Topaz (Jan 03 2021 at 16:11):

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

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

view this post on Zulip 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 ϕ(pq)=(p1)(q1)\phi(pq)=(p-1)(q-1)?

view this post on Zulip Adam Topaz (Jan 03 2021 at 16:14):

Ok maybe I'm not so sure :wink:

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

view this post on Zulip Kevin Buzzard (Jan 03 2021 at 16:15):

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

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

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

view this post on Zulip Adam Topaz (Jan 03 2021 at 16:42):

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

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

view this post on Zulip Arcayn (Jan 04 2021 at 12:39):

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

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

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

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

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

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

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

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

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