[Merged by Bors] - chore: move most of Data/Matrix to LinearAlgebra by grunweg · Pull Request #28966 · leanprover-community/mathlib4

grunweg · 2025-08-26T14:40:29Z

These are not related to data structures at all.
This PR is not exhaustive, likely further files in Data/Matrix should also be moved.

Zulip discussion: #mathlib4 > Cleaning up `Data` @ 💬

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

A future PR will try to remove all topology imports from data as well.

github-actions · 2025-08-26T14:41:37Z

PR summary cefe7b7756

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
`Mathlib.Data.Matrix.Rank`	-1511
`Mathlib.Data.Matrix.Vec`	-1210
`Mathlib.Data.Matrix.Kronecker`	-1208
`Mathlib.Data.Matrix.Hadamard`	-947
`Mathlib.Data.Matrix.Notation`	-943
`Mathlib.Data.Matrix.RowCol`	-936
`Mathlib.Data.Matrix.ConjTranspose`	-935
`Mathlib.Data.Matrix.CharP`	-464
`Mathlib.Data.Matrix.Defs`	-430
`Mathlib.LinearAlgebra.Matrix.Defs`	430
`Mathlib.LinearAlgebra.Matrix.CharP`	464
`Mathlib.LinearAlgebra.Matrix.ConjTranspose`	935
`Mathlib.LinearAlgebra.Matrix.RowCol`	936
`Mathlib.LinearAlgebra.Matrix.Notation`	943
`Mathlib.LinearAlgebra.Matrix.Hadamard`	947
`Mathlib.LinearAlgebra.Matrix.Kronecker`	1208
`Mathlib.LinearAlgebra.Matrix.Vec`	1210
`Mathlib.LinearAlgebra.Matrix.Rank`	1511

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/Matrix/Kronecker.lean` was renamed to `Mathlib/LinearAlgebra/Matrix/Kronecker.lean without a module deprecation
Please create a follow-up pull request adding one. Thanks!

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

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

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

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

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

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

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

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

mathlib4-dependent-issues-bot · 2025-08-26T22:46:58Z

This PR/issue depends on:

~~[Merged by Bors] - chore: remove last Analysis imports from Data #28953~~
By Dependent Issues (🤖). Happy coding!

mathlib4-merge-conflict-bot · 2025-08-26T23:40:55Z

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

YaelDillies

Thanks! Looks like a great idea. Probably all of Matrix can move eventually.

maintainer delegate

Mathlib/LinearAlgebra/CrossProduct.lean

Mathlib/LinearAlgebra/Matrix/Determinant/Basic.lean

Mathlib/LinearAlgebra/Matrix/DotProduct.lean

Mathlib/LinearAlgebra/Matrix/NonsingularInverse.lean

Mathlib/LinearAlgebra/Matrix/Notation.lean

Mathlib/LinearAlgebra/Matrix/ToLin.lean

Mathlib/Tactic/Linter/DirectoryDependency.lean

MathlibTest/matrix.lean

github-actions · 2025-08-27T08:59:42Z

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

grunweg · 2025-08-27T09:39:13Z

This needs a re-shaking: will do this once CI was completed.

YaelDillies · 2025-08-27T10:58:38Z

I think you can simply replace some (but not all) Data.Matrix with LinearAlgebra.Matrix in noshake.json

bryangingechen

Thanks!
bors r+

These are not related to data structures at all. This PR is not exhaustive, likely further files in `Data/Matrix` should also be moved. Zulip discussion: [#mathlib4 > Cleaning up `Data` @ 💬](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Cleaning.20up.20.60Data.60/near/536224905) Co-authored-by: Michael Rothgang <rothgang@math.uni-bonn.de>

mathlib-bors · 2025-08-27T23:00:07Z

Pull request successfully merged into master.

Build succeeded:

CI Success

…y#28966) These are not related to data structures at all. This PR is not exhaustive, likely further files in `Data/Matrix` should also be moved. Zulip discussion: [#mathlib4 > Cleaning up &leanprover-community#96;Data&leanprover-community#96; @ 💬](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Cleaning.20up.20.60Data.60/near/536224905) Co-authored-by: Michael Rothgang <rothgang@math.uni-bonn.de>

github-actions bot added the file-removed A Lean module was (re)moved without a `deprecated_module` annotation label Aug 26, 2025

grunweg force-pushed the small-data branch from fc584a1 to 38a07ac Compare August 26, 2025 14:46

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

github-actions 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 Aug 26, 2025

grunweg force-pushed the small-data branch from 8b85790 to edec275 Compare August 26, 2025 15:28

github-actions bot added merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) and removed merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) labels Aug 26, 2025

grunweg force-pushed the small-data branch from edec275 to a288a7b Compare August 26, 2025 16:31

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 Aug 26, 2025

mathlib4-dependent-issues-bot removed the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label Aug 26, 2025

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 Aug 26, 2025

grunweg force-pushed the small-data branch from a288a7b to 4398d2d Compare August 27, 2025 08:40

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 Aug 27, 2025

grunweg requested a review from YaelDillies August 27, 2025 08:40

grunweg mentioned this pull request Aug 27, 2025

chore: reduce Topology imports in Data #29012

Open

1 task

YaelDillies approved these changes Aug 27, 2025

View reviewed changes

ghost added the maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. label Aug 27, 2025

grunweg added 7 commits August 27, 2025 20:22

Data.Matrix.Defs

4ff8540

Data.Matrix.CharP

4ff5b70

Data.Matrix.Hadamard

337c471

Data.Matrix.Kronecker

efbaee6

A few more files

7f2dff4

Data.Matrix.Notation

dad85ac

chore: remove duplicate line

3e50e63

grunweg added 2 commits August 27, 2025 20:22

order

95d9bef

Update noshake.json

7f6687b

grunweg force-pushed the small-data branch from 6ee0ec1 to 7f6687b Compare August 27, 2025 18:23

bryangingechen approved these changes Aug 27, 2025

View reviewed changes

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 27, 2025

mathlib-bors bot changed the title ~~chore: move most of Data/Matrix to LinearAlgebra~~ [Merged by Bors] - chore: move most of Data/Matrix to LinearAlgebra Aug 27, 2025

mathlib-bors bot closed this Aug 27, 2025

grunweg deleted the small-data branch August 28, 2025 06:23

Conversation

grunweg commented Aug 26, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

github-actions bot commented Aug 26, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

PR summary cefe7b7756

Import changes for modified files

Declarations diff

Uh oh!

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

Uh oh!

mathlib4-merge-conflict-bot commented Aug 26, 2025

Uh oh!

YaelDillies left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

github-actions bot commented Aug 27, 2025

Uh oh!

grunweg commented Aug 27, 2025

Uh oh!

YaelDillies commented Aug 27, 2025

Uh oh!

bryangingechen left a comment

Choose a reason for hiding this comment

Uh oh!

mathlib-bors bot commented Aug 27, 2025

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

5 participants

grunweg commented Aug 26, 2025 •

edited

Loading

github-actions bot commented Aug 26, 2025 •

edited

Loading