refactor(Analysis/NormedSpace/Exponential): remove the 𝕂 argument from exp

[astrainfinita]

This PR builds upon #8370 and avoids Algebra ℚ typeclass assumptions wherever possible.

Many [NormedAlgebra ℚ 𝔸] can be generalized to [NontriviallyNormedField 𝕂] [CharZero 𝕂] [ContinuousSMul ℚ 𝕂] [NormedAlgebra 𝕂 𝔸], which basically means allowing ℚ to use other equivalent norms, and may not be the case of concern.

It might be possible to use some Prop-valued typeclasses to avoid the diamond problem potentially caused by [NormedAlgebra ℚ 𝔸]. This makes it unnecessary to manually obtain [NormedAlgebra ℚ 𝔸] when we have [NormedAlgebra ℝ 𝔸] or [NormedAlgebra ℂ 𝔸].

Co-authored-by: Eric Wieser [email protected]

---

• depends on: [Merged by Bors] - chore(Analysis/SpecificLimits/Basic): generalize lemmas #28475

There are still some documentation comments that need to be updated.

Zulip: #mathlib4 > Real.exp @ 💬

[mathlib4-dependent-issues-bot]

This PR/issue depends on:

• [Merged by Bors] - chore(Analysis/SpecificLimits/Basic): generalize lemmas #28475
  By Dependent Issues (🤖). Happy coding!

[mathlib4-merge-conflict-bot]

This pull request has conflicts, please merge master and resolve them.

[j-loreaux]

I really like this approach, thanks!

[j-loreaux]

Actually, we should say more now, because we're giving a (perfectly reasonable) junk value if 𝔸 can't be equipped with a ℚ-algebra structure.

Some detailed comments about the reason it's being done this way, what problems it solves and how it avoids downsides should be given in the module documentation. Then this docstring should reference the module documentation saying something like: "for details on why this approach is taken, see the module documentation for Mathlib/Analysis/Normed/Algebra/Exponential.lean"

[mathlib4-merge-conflict-bot]

This pull request has conflicts, please merge master and resolve them.