Skip to content

Refactor Riemannian Util layout and simp helpers (#5 #6 #7)#58

Merged
poet77 merged 2 commits into
mainfrom
develop
May 19, 2026
Merged

Refactor Riemannian Util layout and simp helpers (#5 #6 #7)#58
poet77 merged 2 commits into
mainfrom
develop

Conversation

@poet77
Copy link
Copy Markdown
Collaborator

@poet77 poet77 commented May 19, 2026

Summary

Issue Links

Closes #5.
Closes #6.
Closes #7.

Rebase Notes

Validation

  • git diff --check origin/main..develop
  • lake env lean OpenGALib/Riemannian/Util/Simp/OperatorSimp.lean
  • lake build

poet77 added 2 commits May 19, 2026 19:24
Implements issue #5 and #7 by moving Riemannian/Util modules into themed subdirectories, renaming the chart-Jacobian files to CLM/Entries names, and updating direct imports.
Implements issue #6 by merging the connection-Laplacian and divergence simp modules into Util/Simp/OperatorSimp.lean.

CovDerivBridges.lean is intentionally kept as a separate post-LeviCivita bridge module because moving those lemmas into CovDerivSmoothness.lean would introduce an import cycle: CovDerivSmoothness is imported by LeviCivita, while the bridge lemmas depend on LeviCivita definitions.
@poet77 poet77 merged commit 08117d7 into main May 19, 2026
3 checks passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

1 participant