This file contains Unicode characters that might be confused with other characters. If you think that this is intentional, you can safely ignore this warning. Use the Escape button to reveal them.
Status quo
We have three definitions:
Real.exp : ℝ → ℝComplex.exp : ℂ → ℂNormedSpace.exp (𝕂 : Type*) {A : Type*} [...] [Algebra 𝕂 A] : A → A
The first 2 definitions work for specific types, the last one generalizes both but takes an extra argument K
which is used to compute ((n ! : ℕ) : 𝕂)⁻¹ • x ^ n.
Goals
We want to merge these three definitions into one (leanprover-community/mathlib4#8372). The new definition must work at least for Banach algebras over rational, real, complex, and p-adic numbers.
We also want to avoid increasing (or preferably even reduce) the imports necessary for Real.exp.
Approaches
Fix 𝕂 = ℚ in the definition
We can require that our ring is an algebra over rational numbers. We do not require that this is a normed algebra, so the definition works for algebras over p-adic numbers.
The main downside of this approach is that we don't have instances deducing [Algebra ℚ A] from [Algebra ℝ A] or [Algebra ℚ_[p] A].
So, with this approach we have a choice
- either add these instances, opening another door for non-defeq instance diamonds;
- or require users to explicitly assume
[Algebra ℚ A]to work withexp.
Split on the base field
We can leave NormedSpace.exp as is, but merge Real.exp with Complex.exp into a new definition Real.exp that works for any Banach algebra over real numbers. Algebras over p-adics can use NormedSpace.exp directly.
Use DividedPowers
... or a similar typeclass/structure. This approach has the same downsides as fixing the base field to be rational numbers. In addition, using DividedPowers specifically add unnecessary imports to the definition of Real.exp.