Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-08-05 10:42 2b9ac697

View on Github →

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.

Estimated changes