Simplex reindexing PRs

Stream: PR reviews

[Joseph Myers]

I'd like to ping my series of PRs adding lemmas about how Affine.Simplex.reindex interacts with other simplex definitions.

There are two PRs purely in an affine space context: #31054 (interactions with face and faceOpposite) and #31257 (interactions with restrict, setInterior, interior, closedInterior).

The other four PRs deal with interactions with simplex definitions in a Euclidean context. #31056 (interactions with altitude, altitudeFoot, height) depends on #31054; #31057 (interactions with incenter and various associated definitions) depends on #31056. #31210 (mongePoint, mongePlane, orthocenter) and #31256 (signedInfDist) do not depend on any other PRs.

[Joseph Myers]

I'd like to ping this series again. We have #31054, #31210 and #31256 with no unmerged dependencies, #31056 depending on #31054 and #31057 depending on #31056.

I've also started a parallel series of similar lemmas for map and restrict. There, #32019 has no unmerged dependencies (and #32023 is an analogous PR with no unmerged dependencies but not actually about those simplex definitions) and #32021 depends on #32019. The two series may sometimes produce textual merge conflicts because of adding new lemmas to the same places in the same files, but are otherwise independent of each other.

[Joseph Myers]

Thanks for the reviews so far. I'd like to ping the simplex reindex, map and restrict PRs again.

• #31057: feat(Geometry/Euclidean/Incenter): reindex lemmas
• #31210: feat(Geometry/Euclidean/MongePoint): reindex lemmas
• #32019: feat(Geometry/Euclidean/Projection): map and subtype lemmas
• #32021: feat(Geometry/Euclidean/Altitude): map and restrict lemmas (depends on #32019)
• #32270: feat(Geometry/Euclidean/Incenter): map and restrict lemmas (depends on #32021)

The series for reindex is complete (covers all remaining simplex definitions I think are missing such lemmas). The series for map and restrict isn't complete yet (there may be more such PRs in future to add such lemmas for more simplex definitions).

[Joseph Myers]

I'd like to ping #31057 and #32019 (no reviews so far, no open dependencies) again.