Skip to content

Review of the code - #282

Merged
RemyDegenne merged 1 commit into
mainfrom
review
Oct 29, 2026
Merged

RemyDegenne merged 1 commit into
mainfrom
review

Conversation

@RemyDegenne

Copy link
Copy Markdown
Collaborator

AI review of the code. The main changes are:

  • move many lemmas to better places, notably ForMathlib files that mirror Mathlib paths
  • weaken assumptions
  • rename some lemmas

@RemyDegenne
RemyDegenne merged commit 0dc41a5 into main Oct 29, 2026
1 check passed
@RemyDegenne
RemyDegenne deleted the review branch October 29, 2026 18:09
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant