Zulip Chat Archive

Stream: new members

Topic: Proof of Euler's product formula for totient

Stuart Presnell (Nov 13 2021 at 21:08):

I've formalised a proof of Euler's product formula for the totient function φ

(φ n) = n *  p in (prime_divisors n), (1 - p⁻¹:)

I've separately defined prime_divisors and proved a few basic lemmas that are used in the above proof

def prime_divisors (n:) := (divisors n).filter prime

which I guess best belongs in number_theory/divisors.

I'm guessing it would be best to submit the latter material as a PR first, and then if that's accepted I'll submit the product formula proof as another PR separately.

Johan Commelin (Nov 13 2021 at 21:16):

Is divisors available in data.nat.prime? If so, I would add prime_divisors there.

Ruben Van de Velde (Nov 13 2021 at 21:17):

Hmm, I'm surprised we don't have anything like prime_divisors yet - I was looking at docs#nat.factors, but that's with multiplicity

Ruben Van de Velde (Nov 13 2021 at 21:18):

Would it be equal to n.factors.to_finset?

Stuart Presnell (Nov 13 2021 at 21:20):

Johan Commelin said:

Is divisors available in data.nat.prime? If so, I would add prime_divisors there.

Looks like divisors isn't available in data.nat.prime.

Stuart Presnell (Nov 13 2021 at 21:22):

I've seen one or two Zulip threads on the lack of a finset-valued prime divisors function, which no-one seemed to have acted on since the topic came up.

Stuart Presnell (Nov 13 2021 at 21:24):

I briefly had a go at proving that it's equal to list.to_finset (factors n) but didn't finish it, mostly because I didn't need that for what I was doing.

Stuart Presnell (Nov 13 2021 at 21:41):

Ok, I've just added the proof that n.prime_divisors = n.factors.to_finset.

Stuart Presnell (Nov 13 2021 at 21:47):

Would it be better for some reason to define prime_divisors as n.factors.to_finset (and then prove the equality with (divisors n).filter prime as a lemma)?
[Of course, one answer to that question is "Try it and see if it makes anything easier"! But I'm hoping the voice of experience can swoop in to save me from having to try that experiment. :) ]

Stuart Presnell (Nov 13 2021 at 21:59):

Submitted the material on prime_divisors as PR #10318

Kevin Buzzard (Nov 13 2021 at 22:53):

@Chris Birkbeck the product formula should make the "classify roots of unity in cyclotomic fields" question from #FLT regular much easier

Chris Birkbeck (Nov 13 2021 at 22:58):

Yes, this should hopefully help with one of the totient proofs I've been stuck on :)

Stuart Presnell (Nov 13 2021 at 23:35):

Is it easy/reasonable to submit the proof as a PR that depends on the one that's currently under submission (#10318)? Or should I wait until that's accepted and merged?

Stuart Presnell (Nov 13 2021 at 23:39):

While I'm waiting to decide what to do, maybe I can ask for some help in improving the proof. At one point I end up needing to prove the following equality. My first draft was quite messy so I took it out as a lemma to work on it separately. Here's what I ended up with:

lemma euler_lemma1 {p m : } (hm : 0 < m) (hp: 0 < p) :
  p ^ (m - 1) * (p - 1) = p ^ m - p ^ m * (p:)⁻¹  :=
  have hp' : 1  p := by linarith,
  rw [(nat.cast_sub hp'), mul_sub],

  have hm' : 1  m := by linarith,
  have := pow_sub_mul_pow p hm',
  simp at this, rw this, simp,
  rw [this, mul_assoc],

  have hp' : (p:)  0, by {intro H, finish},
  rw mul_inv_cancel hp', simp,

Is there a nicer way to prove this — some clever tactics for working in that I've missed?

Alex J. Best (Nov 13 2021 at 23:54):

Yes its possible to submit PRs that build on each other, and we have tools to help organise this, see e.g. https://github.com/leanprover-community/mathlib/pull/10255 you just have to put

- [ ] depends on: #10318

below the


line in the PR message, and the bots will automatically tag it with appropriate labels and let you know when its ready

Alex J. Best (Nov 13 2021 at 23:56):

In this case you should make the second branch based off of the branch for the first PR so that it all builds sucessfully in both PRs, then when the first is merged you can do git pull master and git push in the second branch to make the new diff against master now

Alex J. Best (Nov 13 2021 at 23:57):

I haven't tried to play with the code, bu I see some casts, so the tactic#norm_cast family (tactic#exact_mod_cast tactic#push_cast tactic#rw_mod_cast etc) might be useful to you. Maybe tactic#field_simps too, which is good for putting things over a common denominator.

Stuart Presnell (Nov 13 2021 at 23:58):

Great, thanks very much

Alex J. Best (Nov 13 2021 at 23:59):

There is also tactic#assoc_rw, which might shave a line off your proof, but it becomes very useful when you have to do a lot of manual mul_assocs

Alex J. Best (Nov 13 2021 at 23:59):

I'd try to avoid using finish in a PR to mathlib if I could, it can be quite slow unfortunately

Alex J. Best (Nov 14 2021 at 00:01):

Also it looks like you have a glossary#non-terminal-simp, which can be quite brittle so we avoid that pattern in mathlib

Stuart Presnell (Nov 14 2021 at 00:13):

Thanks so much for your help!

Kevin Buzzard (Nov 14 2021 at 00:18):

import tactic
import data.rat.basic

lemma euler_lemma1 {p m : } (hm : 0 < m) (hp: 0 < p) :
  p ^ (m - 1) * (p - 1) = p ^ m - p ^ m * (p:)⁻¹  :=
  have : (p : )  0 := by simp [(ne_of_lt hp).symm],
  cases m, cases hm,
  cases p, cases hp,
  simp [nat.succ_eq_add_one],

Stuart Presnell (Nov 14 2021 at 00:28):

Wow, that's so much nicer! Thanks!

Kevin Buzzard (Nov 14 2021 at 00:32):

It's a lazy proof -- I want to solve this by ring so I just keep trying ring until it works. The first problem is that I need to clear denominators so I do this with field_simp but that tactic isn't smart enough to construct the proof that (p : Q) isn't zero so I have to do it myself (I feed in the proof that it's non-zero as a natural because I knew simp could take it from there). The next issue is that you have used natural subtraction twice. For me, this is unidiomatic, because natural subtraction is not a sensible function; lots of things aren't true for it and it screws up automation. For me, hm : 0 < m and m-1 together tell me that you've stated this lemma suboptimally: m should be n+1 and there should be no inequality or natural subtraction, if you can possibly help it; that would save the cases m line and the succ_eq_add_one line; I was proving what was put in front of me, not what I would have formalised myself. Having eliminated both nat subtractions with this cases hack I then have to deal with the fact that my hack introduced succs, which I removed and then finally it worked.

Stuart Presnell (Nov 14 2021 at 00:40):

Ok, I'll see what I can do to reformulate it. I think I can see what I need to change.

Stuart Presnell (Nov 15 2021 at 14:22):

@Ruben Van de Velde suggested a couple of days ago that my definition of prime_divisors should be equal to factors.to_finset, which it turned out was correct, and I might have saved myself some work if I'd paid more attention to that point.

With that in mind I'd like to check whether another definition would be worth having:

def prime_factorization (n:) := (n.factors.to_finset).image (λ p, (p, n.factors.count p))
#eval (prime_factorization 1200)     -- {(2, 4), (3, 1), (5, 2)}   since 1200 = 2^4 * 3^1 * 5^2

Is something like this already defined in mathlib? Is there a nicer way to express it?

Eric Rodriguez (Nov 15 2021 at 14:26):

just don't to_finset it ;b factors is an ordered list of the prime factors, including multiplicity

Eric Rodriguez (Nov 15 2021 at 14:27):

oh, sorry, I read it wrong. anyways, I'm sure there must be a list/multiset function that counts and places them in a pair like that

Alex J. Best (Nov 15 2021 at 14:36):

Is it docs#prime_multiset or something like that?

Stuart Presnell (Nov 15 2021 at 14:45):

In data/pnat/factors we have

factor_multiset (n : +) : prime_multiset

where prime_multiset := multiset nat.primes. So this gives the multiset of prime factors but not explicitly the counts.

Similarly, in data/nat/prime we have

factors :   list 

which is the list of all the prime factors but again not the counts.

Stuart Presnell (Nov 15 2021 at 14:50):

So I suppose whatever purpose might be served by prime_factorization could just as well be served by using factors.to_finset to get the set of prime factors and then extracting the count information by list.count p (factors n).

Eric Rodriguez (Nov 15 2021 at 14:50):

prime_multiset should be burnt to the ground, IMO. and I think if this should exist, this should exist in the form of a function that maps a multiset to a finset of the original thing and its multiplicity

Stuart Presnell (Nov 15 2021 at 15:00):

Ha! It certainly seemed a bit unwieldy when I tried using it, and the fact that factor_multiset takes a pnat rather than a nat added an extra little inconvenience.

Is there not already a function that takes a list L to a list (or finset) of pairs (x, count L x)? (I don't know how I would go about searching for such a function.)

Alex J. Best (Nov 15 2021 at 15:09):

Yes for multiset you still need to take counts, it just seems a more reasonable data type for a prime factorisation than a list

Yaël Dillies (Nov 15 2021 at 15:44):

Eric Rodriguez said:

prime_multiset should be burnt to the ground.

Yes please

Eric Wieser (Nov 15 2021 at 21:13):

Are you looking for docs#multiset.to_finsupp?

Yakov Pechersky (Nov 15 2021 at 21:51):

There's no reason it should be noncomputable.

Alex J. Best (Nov 15 2021 at 21:54):

Finsupp isn't a particularly computable representation of this data though right?

Alex J. Best (Nov 15 2021 at 21:55):

Like if you really wanted to compute something a list of pairs seems much more efficient

Alex J. Best (Nov 15 2021 at 21:56):

That said, I agree a better def than finsupp.to_multiset.symm wouldn't go amiss

Yakov Pechersky (Nov 15 2021 at 21:58):

I agree that finsupp isn't a useful computable notion. But going from multiset X to finset (X x pnat), which is isomorphic to a subset of finsupp, is what was originally asked for.

Stuart Presnell (Nov 15 2021 at 22:04):

So on the one hand we have factors : ℕ → list ℕ with list.count to extract the multiplicities. And on the other hand we have factor_multiset : nat → prime_multiset with multiset.to_finsupp to extract the multiplicities. Given the choice, it seems like factors and count is nicer all round. Are there any advantages to going the multiset route that I'm missing?

Yakov Pechersky (Nov 15 2021 at 22:13):

Did you look at the implementation of multiset.to_finsupp? It also goes through count. What will you be using the counts for? The multiset is more "basic" since there's no inherent order to the prime factorization. The list, iirc, is the result of sorting the prime factors.

Yakov Pechersky (Nov 15 2021 at 22:15):

So I think your proposed implementation above via image is the appropriate one.

Alex J. Best (Nov 15 2021 at 22:16):

Yeah you gain some API by using multiset is all, like a notion of less than or equal (which corresponds to the original numbers being divisible by each other), or being able to take unions and sums of multisets, whats better depends on your use case

Stuart Presnell (Nov 15 2021 at 22:38):

Thanks everyone. I think for now I'll stick with the list-based implementation and see how that goes.

Eric Wieser (Nov 16 2021 at 00:53):

@Yakov Pechersky, its noncomputable because docs#finsupp.has_add is noncomputable and that's one of the arguments to add_equiv.mk

Yakov Pechersky (Nov 16 2021 at 01:02):

Yes, that makes sense. I'm just saying the inv_fun of the equiv, which is the forward direction desired here, is computable.

Stuart Presnell (Nov 18 2021 at 09:37):

After building lots of infrastructure (mostly around prime_factorization) and filling in lots of sorrys I finally have a working sorry-free first draft of the proof. :D

Stuart Presnell (Nov 18 2021 at 09:38):

Now I have a bunch of refactoring and tidying up to do, then I'll be ready to submit it as a PR.

Last updated: Dec 20 2023 at 11:08 UTC