# Zulip Chat Archive

## Stream: general

### Topic: How do you construct a sum over divisors of n?

#### Daniel Donnelly (Jun 14 2022 at 05:16):

I'm new to Lean, but I think a motivating example would help me out, my interests currently don't lie in abstract algebraic, topological, homological etc, but instead on just analysis of arithmetic functions. So show me some code! Simplest code wins.

#### Daniel Donnelly (Jun 14 2022 at 05:17):

Can we do LaTeX here? $\LaTeX$ test

#### Daniel Donnelly (Jun 14 2022 at 05:18):

Yes, if you click your Start ChatJax button,we can see it

#### Junyan Xu (Jun 14 2022 at 05:53):

take a look at docs#nat.arithmetic_function.sigma, src#nat.arithmetic_function.sigma

#### Junyan Xu (Jun 14 2022 at 05:53):

`$$\sigma$$`

$\sigma$

#### Stuart Presnell (Jun 14 2022 at 11:55):

For a simple example of a theorem involving a sum over divisors, how about docs#nat.sum_totient

```
lemma sum_totient (n : ℕ) : n.divisors.sum φ = n
```

(The theorem is called `sum_totient`

, it lives in the `nat`

namespace, and appending the `docs#`

prefix in Zulip makes a link to that theorem in the documentation pages.)

#### Stuart Presnell (Jun 14 2022 at 11:57):

This is the statement that for any natural number `n`

, the sum of the totient function `φ`

over the divisors of `n`

adds to `n`

.

#### Stuart Presnell (Jun 14 2022 at 11:58):

i.e. the statement that you'd normally write as:

$\sum_{d | n} \phi(d) = n$

#### Stuart Presnell (Jun 14 2022 at 12:23):

You could write this more familiarly as `∀ n : ℕ, ∑ d in (divisors n), φ d = n`

, but the convention in mathlib tends toward writing things more concisely where possible.

#### Eric Rodriguez (Jun 14 2022 at 12:38):

Is that syntactically equal or is there a beta reduction involved in the second statement?

#### Eric Wieser (Jun 14 2022 at 15:40):

The first statement is the reduced version of the second

#### Kyle Miller (Jun 14 2022 at 16:04):

@Eric Rodriguez I think it's eta conversion rather than beta reduction

#### Kyle Miller (Jun 14 2022 at 16:05):

You could test it using `dsimp only { beta := ff, eta := ff }`

and turning each one on individually. (Options are documented here at the end.)

#### Eric Rodriguez (Jun 14 2022 at 18:20):

oh interesting, I used to think that `eta`

was solely for structures, I think I just completely misunderstood it. thanks!

Last updated: Dec 20 2023 at 11:08 UTC