Zulip Chat Archive

I'd like to ping a series of geometry PRs and dependencies: #16184 (bundled spheres), #16191 (betweenness in affine spaces), #16278 (succ_above as an equivalence: not a geometry PR itself, but intended for use in them), #16279 (oriented angles between points), #16332 (collinear lemmas), #16644 (affine combinations in relation to subsets of the index type).

I believe all comments on these PRs have been addressed. There are no dependencies between them, so they can be merged in any order, except that once either of #16191 and #16332 is merged, the other one of those PRs will need a minor update. Most of these PRs have followup material ready to PR once they are in.

Joseph Myers (Oct 04 2022 at 11:42):

Thanks for the reviews so far. The current list is #16184, #16278, #16279, #16332, #16644 (all described above), #16733 (betweenness and affine subspaces). There are no dependencies between these PRs; it should be possible to merge them together or separately in any order.

Joseph Myers (Nov 30 2022 at 13:45):

Since geometry PRs (including affine spaces, betweenness and real.angle) have accumulated again, I'd like to ping the current set: #17395 #17485 #17526 #17527 #17528 #17566 #17572 #17601 #17634 #17635 #17636 #17643 #17645 #17659 #17660 #17683 #17722 #17755 (no dependencies between these PRs, can merge separately or together in any order, I hope).

Joseph Myers (Dec 06 2022 at 19:52):

Thanks for the reviews, this series is now down to 11 open PRs needing review (plus two that have just been approved, plus material ready to go for about 5 more depending on various subsets of that 13 and each other).

Affine spaces: #17635 #17659 #17660
Betweenness / convexity: #17527 #17528 #17601 #17755
Euclidean geometry: #17572 #17634 #17645 #17683

(All the real.angle material has now been merged.)

Johan Commelin (Dec 06 2022 at 19:57):

Thanks for this ping!

Joseph Myers (Dec 14 2022 at 12:31):

Thanks for all the further reviews; this series is now down to three open PRs: #17683 (trigonometric lemmas for oriented angles in right-angled triangles), #17843 (second intersection of a line and a sphere), #17912 (betweenness and affine combinations). Once their dependencies are in, I expect the final two PRs in this series to be law of sines / converse of inscribed angles (depends on #17683) and IMO 2019 Q2 (depends on all of the above).

Joseph Myers (Dec 21 2022 at 00:32):

Everything in this series outside of Euclidean geometry is now in. That is, the two remaining open PRs needing review are #17683 and #17843, with the two followups mentioned above planned once their dependencies are in.

Joseph Myers (Jan 04 2023 at 02:33):

I'd like to ping the final two PRs in this series: #17992 (law of sines, converse of inscribed angles) and #17993 (IMO 2019 Q2, depends on #17992).

Joseph Myers (Jan 12 2023 at 12:15):

Now it's #18069 (a series of easy lemmas suggested by Kevin's review of #17993) and #17993 (where I responded to the initial review).

Eric Wieser (Jan 12 2023 at 12:18):

First one was indeed easy, thanks!

Eric Wieser (Jan 12 2023 at 12:20):

Related to geometry in that it's used in angles; can I get you to take a quick look at the premise behind #18105 and see if you agree with it? I think @Junyan Xu is already on top of reviewing the implementation

Kevin Buzzard (Jan 12 2023 at 15:10):

I'm happy with #17993 but was scared to maintainer merge because it depends on a PR which is not yet merged (at the time of writing)

Riccardo Brasca (Jan 17 2023 at 09:05):

@Kevin Buzzard there has been some activity on #17993 since your comment. If you're still OK with it we can merge it.

Kevin Buzzard (Jan 17 2023 at 23:33):

Just had a look -- I'm still OK with it!

Last updated: Dec 20 2023 at 11:08 UTC

leanprover-community / mathlib