Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-12-06 09:40 38375881

View on Github →

feat(linear_algebra/affine_space/independent): affine.simplex.reindex (#17566) Add a definition for remapping a simplex along an equiv of index types, and associated basic API. (Typically of course the two index types are defeq and this is a permutation of indices within the same type, but the definition covers the general case where they might not be defeq.)

Estimated changes