Skip to content

[Merged by Bors] - chore: remove last Analysis imports from Data#28953

Closed
grunweg wants to merge 8 commits intoleanprover-community:masterfrom
grunweg:data-analysis
Closed

[Merged by Bors] - chore: remove last Analysis imports from Data#28953
grunweg wants to merge 8 commits intoleanprover-community:masterfrom
grunweg:data-analysis

Conversation

@grunweg
Copy link
Copy Markdown
Contributor

@grunweg grunweg commented Aug 26, 2025 •
edited
Loading

@grunweg grunweg added the WIP Work in progress label Aug 26, 2025
@github-actions
Copy link
Copy Markdown

github-actions bot commented Aug 26, 2025 •
edited
Loading

PR summary e68729735c

Import changes for modified files

No significant changes to the import graph

Import changes for all files
Files Import difference
Mathlib.Data.Complex.FiniteDimensional -1606
Mathlib.Data.Complex.Cardinality -1449
Mathlib.Data.Complex.Order -1277
Mathlib.Data.Complex.Norm -1276
Mathlib.Analysis.Complex.Norm 1276
Mathlib.Analysis.Complex.Order 1277
Mathlib.Analysis.Complex.Cardinality 1449
Mathlib.LinearAlgebra.Complex.FiniteDimensional 1606

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

note: file Mathlib/Data/Complex/FiniteDimensional.lean` was renamed to `Mathlib/LinearAlgebra/Complex/FiniteDimensional.lean without a module deprecation
Please create a follow-up pull request adding one. Thanks!

note: file Mathlib/Data/Complex/Norm.lean` was renamed to `Mathlib/Analysis/Complex/Norm.lean without a module deprecation
Please create a follow-up pull request adding one. Thanks!

note: file Mathlib/Data/Complex/Order.lean` was renamed to `Mathlib/Analysis/Complex/Order.lean without a module deprecation
Please create a follow-up pull request adding one. Thanks!

note: file Mathlib/Data/Complex/Cardinality.lean` was renamed to `Mathlib/Analysis/Complex/Cardinality.lean without a module deprecation
Please create a follow-up pull request adding one. Thanks!

@github-actions github-actions bot added the file-removed A Lean module was (re)moved without a `deprecated_module` annotation label Aug 26, 2025
@grunweg
Copy link
Copy Markdown
Contributor Author

grunweg commented Aug 26, 2025 •
edited
Loading

Fun times: now, Data/Complex/Order imports only Data/Complex/Norm --- should this also move to analysis?

After moving that, there is Data/Complex/FiniteDimensional --- which is mostly not analysis (rather linear algebra) data stuff, except that it quotes the cardinality results. We don't have a LinearAlgebra/Complex directory, though... should we have one? What is the purpose of Data?

@grunweg grunweg changed the title Data analysis chore: remove last Analysis imports from Data Aug 26, 2025
@grunweg
Copy link
Copy Markdown
Contributor Author

grunweg commented Aug 26, 2025

Moved FiniteDimensional also

@mathlib4-dependent-issues-bot mathlib4-dependent-issues-bot added the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label Aug 26, 2025
@YaelDillies
Copy link
Copy Markdown
Contributor

YaelDillies commented Aug 26, 2025

Fun times: now, Data/Complex/Order imports only Data/Complex/Norm --- should this also move to analysis?

I believe so. The order more generally belongs to RCLike, which is under Analysis already.

@grunweg grunweg mentioned this pull request Aug 26, 2025
Closed
1 task
@grunweg grunweg removed WIP Work in progress blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) labels Aug 26, 2025
@grunweg grunweg requested a review from YaelDillies August 26, 2025 16:16
YaelDillies
YaelDillies approved these changes Aug 26, 2025
View reviewed changes
Copy link
Copy Markdown
Contributor

@YaelDillies YaelDillies left a comment

Choose a reason for hiding this comment

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

etc...

maintainer delegate

@github-actions
Copy link
Copy Markdown

github-actions bot commented Aug 26, 2025

🚀 Pull request has been placed on the maintainer queue by YaelDillies.

@ghost ghost added the maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. label Aug 26, 2025
@mathlib4-dependent-issues-bot
Copy link
Copy Markdown
Collaborator

mathlib4-dependent-issues-bot commented Aug 26, 2025

This PR/issue depends on:

YaelDillies
YaelDillies reviewed Aug 26, 2025
View reviewed changes
Copy link
Copy Markdown
Contributor

@YaelDillies YaelDillies left a comment

Choose a reason for hiding this comment

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

and yet more below

@grunweg
Copy link
Copy Markdown
Contributor Author

grunweg commented Aug 26, 2025

Updated and re-ordered.

@riccardobrasca
Copy link
Copy Markdown
Member

riccardobrasca commented Aug 26, 2025

Very nice, thanks!

bors merge

@ghost ghost added ready-to-merge This PR has been sent to bors. and removed maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. labels Aug 26, 2025
mathlib-bors bot pushed a commit that referenced this pull request Aug 26, 2025
@grunweg
chore: remove last Analysis imports from Data (#28953)
050e3af 
Co-authored-by: Michael Rothgang <rothgang@math.uni-bonn.de>
@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented Aug 26, 2025

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors bot changed the title chore: remove last Analysis imports from Data [Merged by Bors] - chore: remove last Analysis imports from Data Aug 26, 2025
@mathlib-bors mathlib-bors bot closed this Aug 26, 2025
@grunweg grunweg deleted the data-analysis branch August 27, 2025 08:37
FormulaRabbit81 pushed a commit to YaelDillies/mathlib4 that referenced this pull request Aug 30, 2025
@grunweg @FormulaRabbit81
chore: remove last Analysis imports from Data (leanprover-community#2…
6e84f71 
…8953)

Co-authored-by: Michael Rothgang <rothgang@math.uni-bonn.de>
mathlib-bors bot pushed a commit that referenced this pull request Sep 15, 2025
@adomani
chore: module deprecations from #28953 (#29672)
dba1734 
[#general > deprecated_module @ 💬](https://leanprover.zulipchat.com/#narrow/channel/113488-general/topic/deprecated_module/near/539545664)
joelriou pushed a commit to joelriou/mathlib4 that referenced this pull request Oct 2, 2025
@adomani @joelriou
chore: module deprecations from leanprover-community#28953 (leanprove…
48e5e2c 
…r-community#29672)

[#general > deprecated_module @ 💬](https://leanprover.zulipchat.com/#narrow/channel/113488-general/topic/deprecated_module/near/539545664)
zhuyizheng pushed a commit to zhuyizheng/mathlib4 that referenced this pull request Oct 2, 2025
@adomani @zhuyizheng
chore: module deprecations from leanprover-community#28953 (leanprove…
eb7d7c4 
…r-community#29672)

[#general > deprecated_module @ 💬](https://leanprover.zulipchat.com/#narrow/channel/113488-general/topic/deprecated_module/near/539545664)
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@YaelDillies YaelDillies YaelDillies approved these changes

@mattrobball mattrobball mattrobball left review comments

Assignees

No one assigned

Labels

file-removed A Lean module was (re)moved without a `deprecated_module` annotation ready-to-merge This PR has been sent to bors.

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

5 participants

@grunweg @YaelDillies @mathlib4-dependent-issues-bot @riccardobrasca @mattrobball