How do you construct a sum over divisors of n?

Stream: general

[Daniel Donnelly]

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]

Can we do LaTeX here? $\LaTeX$ test

[Daniel Donnelly]

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

[Junyan Xu]

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

[Junyan Xu]

$$\sigma$$ $\sigma$

[Stuart Presnell]

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]

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]

i.e. the statement that you'd normally write as:
$\sum_{d | n} \phi(d) = n$

[Stuart Presnell]

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]

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

[Eric Wieser]

The first statement is the reduced version of the second

[Kyle Miller]

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

[Kyle Miller]

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]

oh interesting, I used to think that eta was solely for structures, I think I just completely misunderstood it. thanks!