Skip to content

[Merged by Bors] - chore(CategoryTheory): clean imports#39610

Closed
qawbecrdtey wants to merge 3 commits into
leanprover-community:masterfrom
qawbecrdtey:categorytheory
Closed

[Merged by Bors] - chore(CategoryTheory): clean imports#39610
qawbecrdtey wants to merge 3 commits into
leanprover-community:masterfrom
qawbecrdtey:categorytheory

Conversation

@qawbecrdtey

Copy link
Copy Markdown
Collaborator

Open in Gitpod

@github-actions

github-actions Bot commented May 20, 2026

Copy link
Copy Markdown

PR summary 500b5d1e62

Import changes for modified files

Dependency changes

File Base Count Head Count Change
Mathlib.CategoryTheory.Monoidal.OfHasFiniteProducts 662 475 -187 (-28.25%)
Mathlib.CategoryTheory.ComposableArrows.Basic 500 467 -33 (-6.60%)
Mathlib.CategoryTheory.Adhesive.Subobject 960 904 -56 (-5.83%)
Mathlib.CategoryTheory.Monad.Basic 422 417 -5 (-1.18%)
Mathlib.CategoryTheory.Monoidal.Internal.Limits 483 481 -2 (-0.41%)
Mathlib.CategoryTheory.Bicategory.Extension 440 439 -1 (-0.23%)
Import changes for all files
Files Import difference
Mathlib.CategoryTheory.Monoidal.OfHasFiniteProducts -187
Mathlib.CategoryTheory.Adhesive.Subobject -56
5 files Mathlib.CategoryTheory.ComposableArrows.Basic Mathlib.CategoryTheory.ComposableArrows.Four Mathlib.CategoryTheory.ComposableArrows.One Mathlib.CategoryTheory.ComposableArrows.Three Mathlib.CategoryTheory.ComposableArrows.Two
-33
3 files Mathlib.CategoryTheory.Monad.Basic Mathlib.CategoryTheory.Monad.Kleisli Mathlib.CategoryTheory.Monad.Types
-5
3 files Mathlib.CategoryTheory.Monoidal.Cartesian.GrpLimits Mathlib.CategoryTheory.Monoidal.Cartesian.Normal Mathlib.CategoryTheory.Monoidal.Internal.Limits
-2
4 files Mathlib.CategoryTheory.Bicategory.Extension Mathlib.CategoryTheory.Bicategory.Kan.Adjunction Mathlib.CategoryTheory.Bicategory.Kan.HasKan Mathlib.CategoryTheory.Bicategory.Kan.IsKan
-1

Declarations diff

No declarations were harmed in the making of this PR! 🐙

You can run this locally as follows
## from your `mathlib4` directory:
git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci

## summary with just the declaration names:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh <optional_commit>

## more verbose report:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh long <optional_commit>

The doc-module for scripts/pr_summary/declarations_diff.sh in the mathlib-ci repository contains some details about this script.


No changes to strong technical debt.
No changes to weak technical debt.

@github-actions github-actions Bot added the t-category-theory Category theory label May 20, 2026
@qawbecrdtey

Copy link
Copy Markdown
Collaborator Author

!bench

@leanprover-radar

leanprover-radar commented May 20, 2026

Copy link
Copy Markdown

Benchmark results for 1e590bb against 024c9d6 are in. No significant results found. @qawbecrdtey

  • 🟥 build//instructions: +7.1G (+0.00%)

Small changes (2✅)

  • build/module/Mathlib.CategoryTheory.Monoidal.Braided.Transport//instructions: -463.5M (-5.80%)
  • build/module/Mathlib.CategoryTheory.Monoidal.Internal.Limits//instructions: -1.2G (-9.65%)

@joelriou

Copy link
Copy Markdown
Contributor

Thanks!

bors merge

@mathlib-triage mathlib-triage Bot added the ready-to-merge This PR has been sent to bors. label May 20, 2026
mathlib-bors Bot pushed a commit that referenced this pull request May 20, 2026
@mathlib-bors

mathlib-bors Bot commented May 20, 2026

Copy link
Copy Markdown
Contributor

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors Bot changed the title chore(CategoryTheory): clean imports [Merged by Bors] - chore(CategoryTheory): clean imports May 20, 2026
@mathlib-bors mathlib-bors Bot closed this May 20, 2026
@qawbecrdtey
qawbecrdtey deleted the categorytheory branch May 20, 2026 15:40
RaggedR pushed a commit to RaggedR/mathlib4 that referenced this pull request May 22, 2026
b-mehta pushed a commit to b-mehta/mathlib4 that referenced this pull request Jun 2, 2026
Bergschaf pushed a commit to Bergschaf/mathlib4 that referenced this pull request Jun 3, 2026
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

ready-to-merge This PR has been sent to bors. t-category-theory Category theory

Projects

None yet

Development

Successfully merging this pull request may close these issues.

3 participants