Arithmetic/geometric mean

[lowasser]

This is Formalizing 100 Theorems number 38. I observe we already have it for rational numbers, and maybe we can count it?

Some of the other examples definitely focus on reals, though, and we don't yet have multiplication (#1353). I swear I come back to it every now and then, but the casework seems unavoidable and exhausting. I might be able to reduce it, and I'm not that far away...

[fredrik-bakke]

I observe we already have it for rational numbers, and maybe we can count it?

I remember discussing this with Egbert, and we concluded that when the list does not specify, we should go by what the listed formalizations implement, in this case probably reals.

[lowasser]

Now that we have squares and square roots of reals, this should be outright easy.

[lowasser]

Whoops, not quite. I see now that the formalization target includes the n-ary case, and we don't have the nth roots necessary to achieve that yet.

[lowasser]

#1740 introduces arbitrary roots, making it possible to state the claim (and hopefully to prove it).