feat: Polynomial.map f strictly decreases the degree if f p.leadingCoeff = 0
#47171
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| name: Label New Contributors | |
| # Written with ChatGPT: https://chat.openai.com/share/3777ceb1-d722-4705-bacd-ba3f04b387be | |
| on: pull_request | |
| jobs: | |
| label-and-report-new-contributor: | |
| runs-on: ubuntu-latest | |
| # Don't run on forks, where we wouldn't have permissions to add the label anyway. | |
| if: github.repository == 'leanprover-community/mathlib4' | |
| permissions: | |
| checks: write | |
| pull-requests: write | |
| contents: read | |
| steps: | |
| - name: Label PR and report count | |
| uses: actions/github-script@v7 | |
| with: | |
| script: | | |
| const creator = context.payload.sender.login | |
| const { owner, repo } = context.repo; | |
| const opts = github.rest.issues.listForRepo.endpoint.merge({ | |
| ...context.issue, | |
| owner, | |
| repo, | |
| creator, | |
| state: 'closed' | |
| }) | |
| const issues = await github.paginate(opts) | |
| const pullRequestCount = issues.length; | |
| // Determine if the creator has 5 or fewer pull requests | |
| if (pullRequestCount <= 5) { | |
| // Add the "new-contributor" label to the current pull request | |
| await github.rest.issues.addLabels({ | |
| issue_number: context.issue.number, | |
| owner, | |
| repo, | |
| labels: ['new-contributor'] | |
| }); | |
| } | |
| // Create a check run with a message about the PR count by this author | |
| const message = `Found ${pullRequestCount} PRs by ${creator}.`; | |
| await github.rest.checks.create({ | |
| owner, | |
| repo, | |
| name: 'New Contributor Check', | |
| head_sha: context.payload.pull_request.head.sha, | |
| status: 'completed', | |
| conclusion: 'neutral', | |
| output: { | |
| title: message, | |
| summary: message, | |
| }, | |
| }); |