mathlib3

2b9ac697 - feat(linear_algebra/affine_space): faces of simplices (#3691)

feat(linear_algebra/affine_space): faces of simplices (#3691) Define a `face` of an `affine_space.simplex` with any given nonempty subset of the vertices, using `finset.mono_of_fin`.