Commit 2022-05-09 02:37 594ceda9

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.