mathlib

27e105d2 - chore(analysis/normed_space/exponential): Make the `𝔸` argument implicit (#13986)

chore(analysis/normed_space/exponential): Make the `𝔸` argument implicit (#13986) `exp 𝕂 𝔸` is now just `exp 𝕂`. This also renames two lemmas that refer to this argument in their name to no longer do so. In a few places we have to add type annotations where they weren't needed before, but nowhere do we need to resort to `@`.