Modular arithmetic

Stream: new members

[Nerya]

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]

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

[Kevin Buzzard]

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]

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

[Adam Topaz]

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

[Kevin Buzzard]

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]

Ok maybe I'm not so sure :wink:

[Nerya]

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

[Kevin Buzzard]

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

[Adam Topaz]

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

[Shing Tak Lam]

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

[Adam Topaz]

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

[Adam Topaz]

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]

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

[Arcayn]

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]

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

[Arcayn]

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]

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]

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

[Arcayn]

(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]

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]

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

[Mark Gerads]

I am having trouble with modular arithmetic. How can this be proved, and can someone add this (with a better name and proof) to mathlib?

lemma modCongruent1 (n1 n3 k : ℤ): n1 % n3 = (n1 + k * n3) % n3 :=
begin
  sorry,
end

[Yaël Dillies]

docs#int.add_mul_mod_self

[Eric Wieser]

@Mark Gerads, did you try library_search?

[Yaël Dillies]

Too late, yael_search was triggered :grinning:

[Mark Gerads]

I tried library_search with 'import all'. I don't know why it wasn't found; maybe because the equation was backward?

[Kevin Buzzard]

My instinct is to write it the other way from the way you wrote it; simplification lemmas h : A = B are often used with rw h so to make it easier to use it's nicer to have A the more complicated thing and B the simpler thing.