Skip to content

Conversation

SnirBroshi
Copy link
Contributor


Open in Gitpod

@SnirBroshi
Copy link
Contributor Author

easy

@github-actions github-actions bot added new-contributor This PR was made by a contributor with at most 5 merged PRs. Welcome to the community! easy < 20s of review time. See the lifecycle page for guidelines. t-algebra Algebra (groups, rings, fields, etc) labels Oct 5, 2025
Copy link

github-actions bot commented Oct 5, 2025

PR summary a2df56f501

Import changes for modified files

No significant changes to the import graph

Import changes for all files
Files Import difference

Declarations diff

+ trace_eq_neg_charpoly_nextCoeff

You can run this locally as follows
## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for script/declarations_diff.sh contains some details about this script.


No changes to technical debt.

You can run this locally as

./scripts/technical-debt-metrics.sh pr_summary
  • The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
  • The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

@mathlib4-merge-conflict-bot mathlib4-merge-conflict-bot added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Oct 8, 2025
@mathlib4-merge-conflict-bot
Copy link
Collaborator

This pull request has conflicts, please merge master and resolve them.

@github-actions github-actions bot removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Oct 9, 2025
@SnirBroshi SnirBroshi force-pushed the feature/trace-charpoly-nextcoeff branch from 41f0249 to edaf1b2 Compare October 11, 2025 20:28
@SnirBroshi SnirBroshi requested a review from b-mehta October 13, 2025 00:11
Copy link
Contributor

@b-mehta b-mehta left a comment

Choose a reason for hiding this comment

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

Thanks!

bors merge

mathlib-bors bot pushed a commit that referenced this pull request Oct 14, 2025
@leanprover-community-mathlib4-bot leanprover-community-mathlib4-bot added the ready-to-merge This PR has been sent to bors. label Oct 14, 2025
@mathlib-bors
Copy link
Contributor

mathlib-bors bot commented Oct 14, 2025

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors bot changed the title feat(LinearAlgebra/Matrix/Charpoly): trace_eq_neg_charpoly_coeff using nextCoeff [Merged by Bors] - feat(LinearAlgebra/Matrix/Charpoly): trace_eq_neg_charpoly_coeff using nextCoeff Oct 14, 2025
@mathlib-bors mathlib-bors bot closed this Oct 14, 2025
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

easy < 20s of review time. See the lifecycle page for guidelines. new-contributor This PR was made by a contributor with at most 5 merged PRs. Welcome to the community! ready-to-merge This PR has been sent to bors. t-algebra Algebra (groups, rings, fields, etc)

Projects

None yet

Development

Successfully merging this pull request may close these issues.

4 participants