Skip to content

[Merged by Bors] - chore(NumberField/Cyclotomic): add statements for the case of power one#30996

Closed
xroblot wants to merge 2 commits intoleanprover-community:masterfrom
xroblot:iscyclo_splitprime
Closed

[Merged by Bors] - chore(NumberField/Cyclotomic): add statements for the case of power one#30996
xroblot wants to merge 2 commits intoleanprover-community:masterfrom
xroblot:iscyclo_splitprime

Conversation

@xroblot
Copy link
Copy Markdown
Collaborator

@xroblot xroblot commented Oct 28, 2025


Open in Gitpod

@github-actions
Copy link
Copy Markdown

github-actions bot commented Oct 28, 2025

PR summary aa78411076

Import changes for modified files

No significant changes to the import graph

Import changes for all files
Files Import difference

Declarations diff

+ eq_span_zeta_sub_one_of_liesOver'
+ inertiaDeg_eq_of_prime
+ inertiaDeg_span_zeta_sub_one'
+ isPrime_span_zeta_sub_one'
+ ncard_primesOver_of_prime
+ ramificationIdx_eq_of_prime
+ ramificationIdx_span_zeta_sub_one'

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).

@github-actions github-actions bot added the t-number-theory Number theory (also use t-algebra or t-analysis to specialize) label Oct 28, 2025
Copy link
Copy Markdown
Member

@riccardobrasca riccardobrasca 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 d+

@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented Oct 28, 2025

✌️ xroblot can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

@ghost ghost added the delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). label Oct 28, 2025
@xroblot
Copy link
Copy Markdown
Collaborator Author

xroblot commented Oct 29, 2025

bors r+

@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented Oct 29, 2025

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors bot changed the title chore(NumberField/Cyclotomic): add statements for the case of power one [Merged by Bors] - chore(NumberField/Cyclotomic): add statements for the case of power one Oct 29, 2025
@mathlib-bors mathlib-bors bot closed this Oct 29, 2025
@xroblot xroblot deleted the iscyclo_splitprime branch February 1, 2026 15:49
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). t-number-theory Number theory (also use t-algebra or t-analysis to specialize)

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants