Preliminary PRs for L-series

Stream: PR reviews

[Michael Stoll]

The following is a list of (fairly small) PRs of additional API lemmas that I found useful when working on L-series:

• #10025 (stuff on natural numbers) (merged)
• #10028 (ZMod) (merged)
• #10029 (real numbers and complex powers of natural numbers) (merged)
• #10034 (complex functions of natural numbers) (merged)
• #10038 (topological sums) (merged)
• #10039 (multiplicative characters) (merged)
• #10087 (Taylor series; this one is not so small) (merged)
• #10112 (order on the complex numbers) (merged)

Reviews are welcome! (The PRs are independent from one another.)

[Michael Stoll]

:ping_pong: :up:

[Michael Stoll]

Can someone perhaps look at #10034, #10039 and/or #10112? They are all quite small PRs just adding a few things.

[Johan Commelin]

Looking right now

[Michael Stoll]

Thanks!