[Merged by Bors] - chore(Data/Real): move analysis files to under Analysis#28909
[Merged by Bors] - chore(Data/Real): move analysis files to under Analysis#28909YaelDillies wants to merge 1 commit intoleanprover-community:masterfrom
Analysis#28909Conversation
My criterion was whether the files imported anything from the `Analysis` folder, and I believe this criterion was spot on.
PR summary 644792174d
|
| Files | Import difference |
|---|---|
Mathlib.Data.Real.Pi.Irrational |
-2392 |
Mathlib.Data.Real.Pi.Leibniz |
-2388 |
Mathlib.Data.Real.Pi.Wallis |
-2382 |
Mathlib.Data.Real.Pi.Bounds |
-1951 |
Mathlib.Data.Real.Cardinality |
-1446 |
Mathlib.Data.Real.Hyperreal |
-1439 |
Mathlib.Analysis.Real.Hyperreal |
1439 |
Mathlib.Analysis.Real.Cardinality |
1446 |
Mathlib.Analysis.Real.Pi.Bounds |
1951 |
Mathlib.Analysis.Real.Pi.Wallis |
2382 |
Mathlib.Analysis.Real.Pi.Leibniz |
2388 |
Mathlib.Analysis.Real.Pi.Irrational |
2392 |
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/Data/Real/Pi/Wallis.lean` was renamed to `Mathlib/Analysis/Real/Pi/Wallis.lean without a module deprecation
Please create a follow-up pull request adding one. Thanks!
note: file Mathlib/Data/Real/Pi/Leibniz.lean` was renamed to `Mathlib/Analysis/Real/Pi/Leibniz.lean without a module deprecation
Please create a follow-up pull request adding one. Thanks!
note: file Mathlib/Data/Real/Pi/Bounds.lean` was renamed to `Mathlib/Analysis/Real/Pi/Bounds.lean without a module deprecation
Please create a follow-up pull request adding one. Thanks!
note: file Mathlib/Data/Real/Hyperreal.lean` was renamed to `Mathlib/Analysis/Real/Hyperreal.lean without a module deprecation
Please create a follow-up pull request adding one. Thanks!
note: file Mathlib/Data/Real/Cardinality.lean` was renamed to `Mathlib/Analysis/Real/Cardinality.lean without a module deprecation
Please create a follow-up pull request adding one. Thanks!
note: file Mathlib/Data/Real/Pi/Irrational.lean` was renamed to `Mathlib/Analysis/Real/Pi/Irrational.lean without a module deprecation
Please create a follow-up pull request adding one. Thanks!
grunweg
left a comment
There was a problem hiding this comment.
All files except Mathlib/Analysis/Real/Cardinality.lean LGTM. I'm not sure about that one - can you explain why you think this is best? (Reverting it from this PR and filing a follow-up with more files also works for me.)
|
My reasoning is that it uses the function |
|
I am convinced. Now, please explain to me why |
|
Thanks! |
|
🚀 Pull request has been placed on the maintainer queue by grunweg. |
|
Was this the last import of |
Wish I knew 😁
No, the same dance needs to be performed for |
|
FYI, I'm working on doing the same dance for complex in #28948. |
|
After that, there will be three remaining files:
|
|
Pull request successfully merged into master. Build succeeded: |
AnalysisAnalysis
Continuation of #28909. Co-authored-by: Michael Rothgang <rothgang@math.uni-bonn.de>
…-community#28909) My criterion was whether the files imported anything from the `Analysis` folder, and I believe this criterion was spot on.
…r-community#28948) Continuation of leanprover-community#28909. Co-authored-by: Michael Rothgang <rothgang@math.uni-bonn.de>
These modules were renamed in #28948 and #28909, and this is semi-autogenerated PR to deprecate the old module names. These are 9 `Data.{Complex, Real}.xxx` files that have been renamed to `Analysis.{Complex, Real}.xxx`. I had forgotten about running `lake exe mk_all` after the deprecated modules had been generated.
These modules were renamed in leanprover-community#28948 and leanprover-community#28909, and this is semi-autogenerated PR to deprecate the old module names. These are 9 `Data.{Complex, Real}.xxx` files that have been renamed to `Analysis.{Complex, Real}.xxx`. I had forgotten about running `lake exe mk_all` after the deprecated modules had been generated.
These modules were renamed in leanprover-community#28948 and leanprover-community#28909, and this is semi-autogenerated PR to deprecate the old module names. These are 9 `Data.{Complex, Real}.xxx` files that have been renamed to `Analysis.{Complex, Real}.xxx`. I had forgotten about running `lake exe mk_all` after the deprecated modules had been generated.
These modules were renamed in leanprover-community#28948 and leanprover-community#28909, and this is semi-autogenerated PR to deprecate the old module names. These are 9 `Data.{Complex, Real}.xxx` files that have been renamed to `Analysis.{Complex, Real}.xxx`. I had forgotten about running `lake exe mk_all` after the deprecated modules had been generated.
These modules were renamed in leanprover-community#28948 and leanprover-community#28909, and this is semi-autogenerated PR to deprecate the old module names. These are 9 `Data.{Complex, Real}.xxx` files that have been renamed to `Analysis.{Complex, Real}.xxx`. I had forgotten about running `lake exe mk_all` after the deprecated modules had been generated.
My criterion was whether the files imported anything from the
Analysisfolder, and I believe this criterion was spot on.