mathlib3

3aea2845 - feat(analysis/normed_space): affine map with findim domain is continuous (#5627)