Skip to content

[Merged by Bors] - chore: delay imports of Rat/Field#14326

Closed
kim-em wants to merge 13 commits intomasterfrom
rat_module
Closed

[Merged by Bors] - chore: delay imports of Rat/Field#14326
kim-em wants to merge 13 commits intomasterfrom
rat_module

Conversation

@kim-em
Copy link
Copy Markdown
Contributor

@kim-em kim-em commented Jul 1, 2024


Open in Gitpod

@kim-em kim-em added awaiting-review awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. labels Jul 1, 2024
@github-actions
Copy link
Copy Markdown

github-actions bot commented Jul 1, 2024

PR summary 399b86366c

Import changes

Dependency changes

File Base Count Head Count Change
Mathlib.Algebra.Module.LinearMap.Basic 502 405 -97 (-19.32%)
Mathlib.Algebra.Module.Basic 488 420 -68 (-13.93%)
Mathlib.Algebra.Ring.Action.Basic 323 306 -17 (-5.26%)
Mathlib.Algebra.Module.LinearMap.Defs 396 392 -4 (-1.01%)
Mathlib.Algebra.Module.LinearMap.End 398 394 -4 (-1.01%)
Mathlib.Algebra.Module.Equiv 415 414 -1 (-0.24%)
Mathlib.GroupTheory.GroupAction.ConjAct 560 559 -1 (-0.18%)
Mathlib.Algebra.Module.Submodule.Basic 589 588 -1 (-0.17%)
Mathlib.Algebra.Ring.Subring.Basic 599 598 -1 (-0.17%)

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/no_lost_declarations.sh short <optional_commit>

## more verbose report:
./scripts/no_lost_declarations.sh <optional_commit>

Copy link
Copy Markdown
Contributor

@Ruben-VandeVelde Ruben-VandeVelde left a comment

Choose a reason for hiding this comment

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

Seems reasonable once you shake

@github-actions github-actions bot removed the awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. label Jul 2, 2024
Copy link
Copy Markdown
Contributor

@grunweg grunweg left a comment

Choose a reason for hiding this comment

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

maintainer merge

@github-actions
Copy link
Copy Markdown

github-actions bot commented Jul 2, 2024

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

@github-actions github-actions bot added the maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. label Jul 2, 2024
@sgouezel
Copy link
Copy Markdown
Contributor

sgouezel commented Jul 2, 2024

bors r+

@github-actions github-actions bot added ready-to-merge This PR has been sent to bors. and removed awaiting-review labels Jul 2, 2024
mathlib-bors bot pushed a commit that referenced this pull request Jul 2, 2024
@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented Jul 2, 2024

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors bot changed the title chore: delay imports of Rat/Field [Merged by Bors] - chore: delay imports of Rat/Field Jul 2, 2024
@mathlib-bors mathlib-bors bot closed this Jul 2, 2024
@mathlib-bors mathlib-bors bot deleted the rat_module branch July 2, 2024 08:46
dagurtomas pushed a commit that referenced this pull request Jul 2, 2024
@adomani adomani mentioned this pull request Aug 1, 2024
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. ready-to-merge This PR has been sent to bors.

Projects

None yet

Development

Successfully merging this pull request may close these issues.

4 participants