mathlib

e2f56961 - feat(analysis/normed_space/exponential): add `pi.exp_apply` (#13488)

feat(analysis/normed_space/exponential): add `pi.exp_apply` (#13488) The statement is a bit weird, but this structure is useful because it allows us to push `exp` through `matrix.diagonal` and into its elements.