Skip to content

auto-task(QuantumInfo.ClassicalInfo.Capacity): minimize imports#1455

Merged
jstoobysmith merged 1 commit into
leanprover-community:masterfrom
Alex-Zughaid:auto-importminimizer-20260722-094135
Jul 23, 2026
Merged

auto-task(QuantumInfo.ClassicalInfo.Capacity): minimize imports#1455
jstoobysmith merged 1 commit into
leanprover-community:masterfrom
Alex-Zughaid:auto-importminimizer-20260722-094135

Conversation

@Alex-Zughaid

Copy link
Copy Markdown
Contributor

Summary

Minimizes the imports of QuantumInfo/ClassicalInfo/Capacity.lean.

The file only defines Code, FixedLengthCode, and BlockCode structures over
List, Fin, and — it never uses anything from QuantumInfo.ClassicalInfo.Entropy
(entropy/probability/channel definitions), nor Fintype/Finset instances for Fin.
Replaced the three imports with the single, more basic import that the file actually
needs for its Fin block_in/Fin block_out usage:

  • Removed QuantumInfo.ClassicalInfo.Entropy (unused)
  • Removed Mathlib.Data.Finset.Fin (unused)
  • Removed Mathlib.Data.Fintype.Fin (unused; replaced by the more basic Mathlib.Data.Fin.Basic)

Downstream impact

None. QuantumInfo.ClassicalInfo.Capacity is not imported by any other file in the
repo (its import in QuantumInfo.lean is commented out), so no other files needed
changes.

Verification

  • lake build QuantumInfo.ClassicalInfo.Capacity — succeeds (510 jobs, down from 2216
    with the original imports)
  • lake build QuantumInfo — succeeds (8733 jobs)
  • lake build Physlib — succeeds (4448 jobs)

No sorrys or axioms were added; only import lines were touched.

Co-authored-by: Claude <noreply@anthropic.com>
@github-actions

Copy link
Copy Markdown
Contributor

Thank you for this PR, which will now be reviewed. If submitting to ./Physlib or ./QuantumInfo, please see our review guidelines if you are not familiar with the process. You should expect a back and forth with a reviewer before your PR is merged. See also that link for how to add appropriate labels to your PR. The PR will also go through a number of automated checks. You can learn more about these here, including how to run them locally.

If you are submitting to ./PhyslibAlpha there will be a lighter review process, though your PR must still pass the automated checks.

If you want to bring attention to this PR, please write a message on this thread of the Lean Zulip.

Important: If a reviewer adds an awaiting-author label to your PR, once you have addressed the review comments, please remove that label by adding a comment with -awaiting-author. This helps us keep track of reviews.

@jstoobysmith jstoobysmith left a comment

Copy link
Copy Markdown
Member

Choose a reason for hiding this comment

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

Thanks Alex, I've approved this one and will merge it once the Linters finish.

@jstoobysmith jstoobysmith added the ready-to-merge This PR is approved and will be merged shortly label Jul 22, 2026
@jstoobysmith
jstoobysmith merged commit c7f3638 into leanprover-community:master Jul 23, 2026
8 checks passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

ready-to-merge This PR is approved and will be merged shortly t-classical-info-qi

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants