# 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:ℚ)⁻¹ :=
begin
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,
end
```

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_assoc`

s

#### 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:ℚ)⁻¹ :=
begin
have : (p : ℚ) ≠ 0 := by simp [(ne_of_lt hp).symm],
field_simp,
cases m, cases hm,
cases p, cases hp,
simp [nat.succ_eq_add_one],
ring_exp,
end
```

#### 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 `sorry`

s 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