Skip to content

Rocqnavi functional analysis#2020

Open
yoshihiro503 wants to merge 2 commits into
math-comp:masterfrom
proof-ninja:yoshihiro503@rocqnavi-functional_analysis
Open

Rocqnavi functional analysis#2020
yoshihiro503 wants to merge 2 commits into
math-comp:masterfrom
proof-ninja:yoshihiro503@rocqnavi-functional_analysis

Conversation

@yoshihiro503

Copy link
Copy Markdown
Contributor
Motivation for this change

fixes #2018

Checklist
  • added corresponding entries in CHANGELOG_UNRELEASED.md
  • added corresponding documentation in the headers

Reference: How to document

Merge policy

As a rule of thumb:

  • PRs with several commits that make sense individually and that
    all compile are preferentially merged into master.
  • PRs with disorganized commits are very likely to be squash-rebased.
Reminder to reviewers

@yoshihiro503 yoshihiro503 force-pushed the yoshihiro503@rocqnavi-functional_analysis branch from 6e8461c to 4bcd010 Compare July 8, 2026 07:48
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.

Rocqnavi: The dependency file graph don't have functinal_analysis

1 participant