mathlib

594ceda9 - feat(analysis/normed_space/exponential): Generalize `field` lemmas to `division_ring` (#13997)

feat(analysis/normed_space/exponential): Generalize `field` lemmas to `division_ring` (#13997) This generalizes the lemmas about `exp 𝕂 𝕂` to lemmas about `exp 𝕂 𝔸` where `𝔸` 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, since `division_ring` is a mouthful, and really the name reflects the use of `/` in the definition.