Theorem Affine.Simplex.mongePoint_reindex

Modification history

2025-12-05 16:31

Mathlib/Geometry/Euclidean/MongePoint.lean

feat(Geometry/Euclidean/MongePoint): `reindex` lemmas (#31210) …

Added Affine.Simplex.mongePoint_reindex View on Github →