feat(LinearAlgebra/AffineSpace): add Desargues's theorem#37456
feat(LinearAlgebra/AffineSpace): add Desargues's theorem#37456Robertboy18 wants to merge 6 commits intoleanprover-community:masterfrom
Conversation
github-actions
bot
added
the
new-contributor
Welcome new contributor!Thank you for contributing to Mathlib! If you haven't done so already, please review our contribution guidelines, as well as the style guide and naming conventions. In particular, we kindly remind contributors that we have guidelines regarding the use of AI when making pull requests. We use a review queue to manage reviews. If your PR does not appear there, it is probably because it is not successfully building (i.e., it doesn't have a green checkmark), has the If you haven't already done so, please come to https://leanprover.zulipchat.com/, introduce yourself, and mention your new PR. Thank you again for joining our community. |
PR summary 9243d59d8cImport changes for modified filesNo significant changes to the import graph Import changes for all files
Declarations diff
You can run this locally as follows## summary with just the declaration names:
./scripts/pr_summary/declarations_diff.sh <optional_commit>
## more verbose report:
./scripts/pr_summary/declarations_diff.sh long <optional_commit>The doc-module for No changes to technical debt.You can run this locally as
|
There was a problem hiding this comment.
Pull request overview
Adds an affine/parallel version of Desargues’s theorem to the affine-geometry portion of Mathlib, and wires it into the umbrella import and the “100 theorems” index.
Changes:
- Introduce
parallel_third_side_of_perspectiveproving the “two pairs of corresponding sides parallel ⇒ third pair parallel” statement under perspective and noncollinearity hypotheses. - Add a
public importof the new module inMathlib.lean. - Point 100-theorems entry #87 to the new declaration in
docs/100.yaml.
Reviewed changes
Copilot reviewed 3 out of 3 changed files in this pull request and generated 1 comment.
| File | Description |
|---|---|
| Mathlib/LinearAlgebra/AffineSpace/Desargues.lean | New file containing the affine Desargues theorem and proof via exists_eq_smul_of_parallel. |
| Mathlib.lean | Exposes the new Desargues module via public import. |
| docs/100.yaml | Updates theorem #87 to reference the new declaration and author. |
💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.
| If two triangles are in perspective from a point, and two pairs of corresponding sides are | ||
| parallel, then the third pair of corresponding sides are also parallel. |
There was a problem hiding this comment.
This is not the full Desargues's theorem, right? The full version also allows non-parallel case (and the conclusion is the 3 intersections are collinear)
There was a problem hiding this comment.
There was a problem hiding this comment.
It looks weird to me... The statement posted for HOL Light (https://www.cs.ru.nl/~freek/100/hol.html#87) looks closer to what I had in mind
There was a problem hiding this comment.
Oh I see, i actually followed the Frédérique Guilhot statement (in coq-community/HighSchoolGeometry):
|
Hey, can you please disclose any AI usage? (per the guidelines linked above) Also your PR description currently mentions Mathlib's 87th PR, and you deleted both the separator and button from the PR template. Can you fix these issues? |
This PR adds an affine (parallel) version of Desargues's theorem!
Main changes
Mathlib/LinearAlgebra/AffineSpace/Desargues.leanwithparallel_third_side_of_perspective: if two triangles are in perspective from a pointSandtwo pairs of corresponding sides are parallel, then the third pair of sides is parallel.
public importtoMathlib.lean.docs/100.yaml(entry [Merged by Bors] - fix: add precedence for guardExpr #87) to point to the new declaration.High level Proof idea is from the rocq repository!
Compare side vectors via
exists_eq_smul_of_parallelfor the two given pairs of parallel sides; theshared comparison along
SAforces the same scalar, yielding parallelism of the third sides.Tests:
lake build Mathlib.LinearAlgebra.AffineSpace.Desargues!