mathlib

82dced60 - feat(analysis/normed_space/finite_dimension): Riesz theorem on compact unit ball and finite dimension (#9147)