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 Ebert, and we concluded that when the list does not specify, we should go by what the listed formalizations implement, in this case probably reals.