[Merged by Bors] - chore(NumberField): create directory Cyclotomic and move relevant files there#30536
[Merged by Bors] - chore(NumberField): create directory Cyclotomic and move relevant files there#30536xroblot wants to merge 2 commits intoleanprover-community:masterfrom
Cyclotomic and move relevant files there#30536Conversation
PR summary c48ea032ed
|
| Files | Import difference |
|---|---|
Mathlib.NumberTheory.Cyclotomic.PID |
-3028 |
Mathlib.NumberTheory.Cyclotomic.Three |
-3010 |
Mathlib.NumberTheory.Cyclotomic.Embeddings |
-2859 |
Mathlib.NumberTheory.Cyclotomic.Rat |
-2520 |
Mathlib.NumberTheory.NumberField.Cyclotomic.Basic |
2520 |
Mathlib.NumberTheory.NumberField.Cyclotomic.Embeddings |
2859 |
Mathlib.NumberTheory.NumberField.Cyclotomic.Three |
3010 |
Mathlib.NumberTheory.NumberField.Cyclotomic.PID |
3028 |
Declarations diff
No declarations were harmed in the making of this PR! 🐙
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
relativevalue is the weighted sum of the differences with weight given by the inverse of the current value of the statistic. - The
absolutevalue is therelativevalue divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).
note: file Mathlib/NumberTheory/Cyclotomic/Embeddings.lean` was renamed to `Mathlib/NumberTheory/NumberField/Cyclotomic/Embeddings.lean without a module deprecation
Please create a follow-up pull request adding one. Thanks!
note: file Mathlib/NumberTheory/Cyclotomic/Three.lean` was renamed to `Mathlib/NumberTheory/NumberField/Cyclotomic/Three.lean without a module deprecation
Please create a follow-up pull request adding one. Thanks!
note: file Mathlib/NumberTheory/Cyclotomic/PID.lean` was renamed to `Mathlib/NumberTheory/NumberField/Cyclotomic/PID.lean without a module deprecation
Please create a follow-up pull request adding one. Thanks!
note: file Mathlib/NumberTheory/Cyclotomic/Rat.lean` was renamed to `Mathlib/NumberTheory/NumberField/Cyclotomic/Basic.lean without a module deprecation
Please create a follow-up pull request adding one. Thanks!
|
Thanks! bors merge |
|
Pull request successfully merged into master. Build succeeded: |
Cyclotomic and move relevant files thereCyclotomic and move relevant files there
…iles there (leanprover-community#30536) Create the directory `NumberTheory/NumberField/Cyclotomic` and move there the files concerning cyclotomic fields over `ℚ`. Deprecated modules files are added in leanprover-community#30583
…er-community#30583) Create the deprecated module files for the files moved in leanprover-community#30536
…iles there (leanprover-community#30536) Create the directory `NumberTheory/NumberField/Cyclotomic` and move there the files concerning cyclotomic fields over `ℚ`. Deprecated modules files are added in leanprover-community#30583
…er-community#30583) Create the deprecated module files for the files moved in leanprover-community#30536
Create the directory
NumberTheory/NumberField/Cyclotomicand move there the files concerning cyclotomic fields overℚ.Deprecated modules files are added in #30583