Analysis.NormedSpace.logarithm?

Stream: Is there code for X?

[Siddharth Bhat]

In a discussion with @Eric Wieser , where I wanted to compute square roots of unit quaternions, it was drawn to my attention that Analysis.NormedSpace.logarithm is missing?

• Is there a different way to compute and reason with quaternion square roots in mathlib as of today?
• Does the "standard power series" for log(1 + x) just work for banach algebras? Does it get more subtle?

[Michael Stoll]

I'm about to PR stuff that would lead to the power series for the complex log. Not sure if that would help.

[Siddharth Bhat]

Does it build the general theory for banach algebras and then specialize to $\mathbb C$? If so, I hope it will "just work " for quaternions!

[Eric Wieser]

I doubt it; we don't even do that for docs#Complex.exp

[Michael Stoll]

You can look at this file and try to figure out whether it generalizes.