mathlib

9c7f0987 - feat(analysis/normed_space/exponential): Generalize `field` lemmas about `exp 𝕂 𝕂` to `division_ring` lemmas about `exp 𝕂 𝔸`

feat(analysis/normed_space/exponential): Generalize `field` lemmas about `exp 𝕂 𝕂` to `division_ring` lemmas about `exp 𝕂 𝔸` All of these lemmas are true when `𝕂` and `𝔸` are different; all we require is that `𝔸` is a `division_ring`. This moves the lemmas down to the appropriate division_ring sections, and replaces the word `field` with `div` in their names.