Skip to content

feat(Geometry/Curve): add Frenet–Serret framework #38348

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
mirajcs wants to merge 17 commits into
base: master
Choose a base branch
from
+504 −0
Open

feat(Geometry/Curve): add Frenet–Serret framework #38348

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
17 commits
Select commit Hold shift + click to select a range
ecc13e4
basic definitions and theorems about curves
mirajcs Apr 21, 2026
165ac89
Merge branch 'leanprover-community:master' into curves
mirajcs Apr 21, 2026
aee1b73
proved deriv_normal and deriv_binormal
mirajcs Apr 21, 2026
55ec921
[pre-commit.ci lite] apply automatic fixes
pre-commit-ci-lite[bot] Apr 21, 2026
9046999
chore: regenerate import files
mirajcs Apr 21, 2026
f68e8cb
fix: declare Geometry.Curves.Basic as a module for Mathlib import
mirajcs Apr 22, 2026
5b40790
Merge branch 'master' into curves
mirajcs Apr 22, 2026
ae44e12
docs: add declaration docstring for ℝ³ notation
mirajcs Apr 22, 2026
b448c97
Merge branch 'master' into curves
mirajcs Apr 22, 2026
6e5ca55
refactor(Curves): generalize part of the Frenet frame via Gram-Schmid…
mirajcs Apr 22, 2026
de39125
Merge branch 'master' into curves
mirajcs Apr 22, 2026
d229432
added forgotten isArcLengthParametrization
mirajcs Apr 22, 2026
00bef13
Merge branch 'master' into curves
mirajcs Apr 22, 2026
1f99e30
Merge branch 'master' into curves
mirajcs Apr 23, 2026
0ef64d3
Merge branch 'master' into curves
mirajcs Apr 26, 2026
6e9bcc5
ci: configure Lean before style lint action
mirajcs Apr 26, 2026
6c4aa41
Merge branch 'master' into curves
mirajcs Apr 27, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
6 changes: 6 additions & 0 deletions .github/workflows/build_template.yml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -768,6 +768,12 @@ jobs:
name: Lint style
runs-on: ubuntu-latest
steps:
- name: Configure Lean
uses: leanprover/lean-action@c544e89643240c6b398f14a431bcdc6309e36b3e # v1.4.0
with:
auto-config: false
use-github-cache: false
use-mathlib-cache: false
Comment on lines +771 to +776
Copy link
Copy Markdown
Collaborator

@wwylele wwylele Apr 26, 2026

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Please don't make changes to CI in an unrelated PR.

Copy link
Copy Markdown
Author

@mirajcs mirajcs Apr 27, 2026

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Thank you for pointing that out. I apologize for modifying the CI configuration in an unrelated PR, that was not intentional. I’ll make sure to keep such changes separate and scoped appropriately in the future.

- uses: leanprover-community/lint-style-action@a7e7428fa44f9635d6eb8e01919d16fd498d387a # 2025-08-18
with:
mode: check
Expand Down
1 change: 1 addition & 0 deletions Mathlib.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -4449,6 +4449,7 @@ public import Mathlib.Geometry.Convex.Cone.DualFinite
public import Mathlib.Geometry.Convex.Cone.Pointed
public import Mathlib.Geometry.Convex.Cone.Simplicial
public import Mathlib.Geometry.Convex.Cone.TensorProduct
public import Mathlib.Geometry.Curves.Basic
public import Mathlib.Geometry.Diffeology.Basic
public import Mathlib.Geometry.Euclidean.Altitude
public import Mathlib.Geometry.Euclidean.Angle.Bisector
Expand Down
Loading
Loading