mathlib3

d9a51803 - refactor(linear_algebra,analysis/normed_space): use `finite`, review API, golf (#17320)

refactor(linear_algebra,analysis/normed_space): use `finite`, review API, golf (#17320) * replace `fintype_of_fin_dim_affine_independent` with `finite_of_fin_dim_affine_independent`; * rename old `finite_of_fin_dim_affine_independent` to `finite_set_of_fin_dim_affine_independent`, generalize; * define `affine_basis.comp_equiv`; * add `affine_basis.finite`, `affine_basis.finite_set`, `affine_basis.coord_apply_centroid`, `affine_basis.card_eq_finrank_add_one` * use more precise statement in `exists_affine_basis`, add `exists_affine_subbasis`; * rename `interior_convex_hull_aff_basis` to `affine_basis.interior_convex_hull`; * rename `exists_subset_affine_independent_span_eq_top_of_open` to `is_open.exists_between_affine_independent_span_eq_top`, golf; * add `is_open.exists_subset_affine_independent_span_eq_top`, `is_open.affine_span_eq_top`, `affine_span_eq_top_of_nonempty_interior`, and `affine_basis.centroid_mem_interior_convex_hull`; * rename `interior_convex_hull_nonempty_iff_aff_span_eq_top` to `interior_convex_hull_nonempty_iff_affine_span_eq_top`