[Merged by Bors] - feat(Geometry/Polygon): nondegeneracy conditions and interconversion with Affine.Triangle by A-M-Berns · Pull Request #34598 · leanprover-community/mathlib4

A-M-Berns · 2026-01-30T04:07:18Z

This PR implements suggestions provided in this comment by @jsm28: interconversion between Polygon P 3 and Affine.Triangle as well as the nondegeneracy conditions NondegenerateVertices and NondegenerateEdges. I tried to keep typeclass restrictions as minimal as possible.

…angles This introduces basic polygon definitions: - `Polygon P n`: vertices indexed by `Fin n` in any type - `EuclideanPolygon n`: polygon in 2D Euclidean space with `n ≥ 3` - `EuclideanTriangle`: non-degenerate triangle with `Affine.Triangle` compatibility Provides edge representations in both affine (`edgePath`, `edgeSet`) and module (`edgePathModule`, `side`) settings, with equivalence theorems. With help from Claude Code (Opus 4.5).

github-actions · 2026-01-30T04:08:42Z

✅ PR Title Formatted Correctly

The title of this PR has been updated to match our commit style conventions.
Thank you!

github-actions · 2026-01-30T04:21:51Z

PR summary 0e4799ceff

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

Declarations diff

+ HasNondegenerateEdges
+ HasNondegenerateEdges.two_le
+ HasNondegenerateVertices
+ HasNondegenerateVertices.hasNondegenerateEdges
+ HasNondegenerateVertices.three_le
+ toPolygon
+ toPolygon_hasNondegenerateVertices
+ toPolygon_toTriangle
+ toPolygon_vertices
+ toTriangle
+ toTriangle_points
+ toTriangle_toPolygon

You can run this locally as follows

## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for scripts/declarations_diff.sh contains some details about this script.

No changes to technical debt.

You can run this locally as

./scripts/technical-debt-metrics.sh pr_summary

The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

jsm28 · 2026-01-30T14:23:49Z

Additional suggested lemmas: NondegenerateEdges implies n is at least 2, and NondegenerateVertices implies it's at least 3.

A-M-Berns · 2026-01-30T22:54:49Z

I've edited the file based on the feedback. I changed the variable (R) to variable (R) in for relevant results, changed NondegenerateVertices to use AffineIndependent, and added the two suggested lemmas.

eric-wieser · 2026-02-13T15:45:06Z

Could you merge master and resolve the conflicts?

Co-authored-by: Johan Commelin <[email protected]>

A-M-Berns · 2026-02-18T20:45:58Z

-awaiting-author

ocfnash

Thanks!

bors merge

@jsm28

…with Affine.Triangle (#34598) This PR implements suggestions provided in [this comment](#34393 (comment)) by @jsm28: interconversion between `Polygon P 3` and `Affine.Triangle` as well as the nondegeneracy conditions `NondegenerateVertices` and `NondegenerateEdges`. I tried to keep typeclass restrictions as minimal as possible. Co-authored-by: AnsonBerns <[email protected]> Co-authored-by: A. M. Berns <[email protected]>

mathlib-bors · 2026-02-25T17:27:58Z

Pull request successfully merged into master.

Build succeeded:

@jsm28

…with Affine.Triangle (leanprover-community#34598) This PR implements suggestions provided in [this comment](leanprover-community#34393 (comment)) by @jsm28: interconversion between `Polygon P 3` and `Affine.Triangle` as well as the nondegeneracy conditions `NondegenerateVertices` and `NondegenerateEdges`. I tried to keep typeclass restrictions as minimal as possible. Co-authored-by: AnsonBerns <[email protected]> Co-authored-by: A. M. Berns <[email protected]>

@jsm28

…with Affine.Triangle (leanprover-community#34598) This PR implements suggestions provided in [this comment](leanprover-community#34393 (comment)) by @jsm28: interconversion between `Polygon P 3` and `Affine.Triangle` as well as the nondegeneracy conditions `NondegenerateVertices` and `NondegenerateEdges`. I tried to keep typeclass restrictions as minimal as possible. Co-authored-by: AnsonBerns <[email protected]> Co-authored-by: A. M. Berns <[email protected]>

A-M-Berns added 16 commits January 25, 2026 02:19

Merge branch 'master' into polygon-basic-clean

a64a34b

Implemented changes suggested by PR comments.

6251190

Added module for CI checks

41485b5

Fixed import

29bf390

Merge branch 'master' into polygon-basic-clean

c5eced2

Fixed more CI issues

09a6303

Merge branch 'master' into polygon-basic-clean

222d2b7

Implemented suggestions

4f8c786

Merge branch 'master' into polygon-basic-clean

772fe48

Merge branch 'master' into polygon-basic-clean

25792f2

Implemented suggestion by @jcommelin

bf46fe0

Rebuilt imports

e27e95c

Deleted extra file

e757648

Fixed CI issues

0edbd00

Second PR

1588549

github-actions bot added new-contributor This PR was made by a contributor with at most 5 merged PRs. Welcome to the community! merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) labels Jan 30, 2026

A-M-Berns changed the title ~~feat(Geometry/Polygon): nondegeneracy conditions and interconversion with Affine.Triangle~~ feat(Geometry/Polygon): nondegeneracy conditions and interconversion with Affine.Triangle Jan 30, 2026

A-M-Berns added 3 commits January 30, 2026 04:12

Merge remote-tracking branch 'origin/master' into affinetriangle

7508497

Trigger CI

7c4a90c

Merged upstream/master

92ff3af

github-actions bot removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Jan 30, 2026

jsm28 reviewed Jan 30, 2026

View reviewed changes

Comment thread Mathlib/Geometry/Polygon/Basic.lean Outdated

Comment thread Mathlib/Geometry/Polygon/Basic.lean Outdated

Comment thread Mathlib/Geometry/Polygon/Basic.lean Outdated

jsm28 reviewed Jan 30, 2026

View reviewed changes

Comment thread Mathlib/Geometry/Polygon/Basic.lean Outdated

Implemented reviewer suggestions

e41f55b

jcommelin reviewed Feb 2, 2026

View reviewed changes

Comment thread Mathlib/Geometry/Polygon/Basic.lean Outdated

Comment thread Mathlib/Geometry/Polygon/Basic.lean Outdated

jcommelin added the awaiting-author A reviewer has asked the author a question or requested changes. label Feb 2, 2026

A-M-Berns added 2 commits February 2, 2026 19:16

Rename Nondegenerate to HasNondegenerate

0042ff8

retrigger CI

d14210b

github-actions bot removed the awaiting-author A reviewer has asked the author a question or requested changes. label Feb 3, 2026

mathlib-triage bot assigned jsm28 Feb 7, 2026

jsm28 reviewed Feb 7, 2026

View reviewed changes

Comment thread Mathlib/Geometry/Polygon/Basic.lean Outdated

Comment thread Mathlib/Geometry/Polygon/Basic.lean Outdated

removed DivisionRing

feb0004

A-M-Berns mentioned this pull request Feb 10, 2026

feat(Geometry/Polygon): simple polygons and boundary map #35069

Open

1 task

used finRotate per PR leanprover-community#35229

bda831c

eric-wieser added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Feb 13, 2026

Merge branch 'master' into affinetriangle

df0b688

github-actions bot removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Feb 13, 2026

A-M-Berns requested a review from jcommelin February 14, 2026 19:47

jcommelin reviewed Feb 18, 2026

View reviewed changes

jcommelin added the awaiting-author A reviewer has asked the author a question or requested changes. label Feb 18, 2026

A-M-Berns and others added 2 commits February 18, 2026 11:14

Apply suggestion from @jcommelin

8311294

Co-authored-by: Johan Commelin <[email protected]>

Apply suggestions by @jcommelin

1afdb07

Co-authored-by: Johan Commelin <[email protected]>

github-actions bot removed the awaiting-author A reviewer has asked the author a question or requested changes. label Feb 18, 2026

ocfnash approved these changes Feb 25, 2026

View reviewed changes

mathlib-triage bot added ready-to-merge This PR has been sent to bors. and removed maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. labels Feb 25, 2026

mathlib-bors bot changed the title ~~feat(Geometry/Polygon): nondegeneracy conditions and interconversion with Affine.Triangle~~ [Merged by Bors] - feat(Geometry/Polygon): nondegeneracy conditions and interconversion with Affine.Triangle Feb 25, 2026

mathlib-bors bot closed this Feb 25, 2026

Conversation

A-M-Berns commented Jan 30, 2026

Uh oh!

github-actions bot commented Jan 30, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

✅ PR Title Formatted Correctly

Uh oh!

github-actions bot commented Jan 30, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

PR summary 0e4799ceff

Import changes for modified files

Declarations diff

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

jsm28 commented Jan 30, 2026

Uh oh!

A-M-Berns commented Jan 30, 2026

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

eric-wieser commented Feb 13, 2026

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

A-M-Berns commented Feb 18, 2026

Uh oh!

ocfnash left a comment

Choose a reason for hiding this comment

Uh oh!

mathlib-bors bot commented Feb 25, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

6 participants

github-actions bot commented Jan 30, 2026 •

edited

Loading

github-actions bot commented Jan 30, 2026 •

edited

Loading