auto-task(QuantumInfo.ClassicalInfo.Capacity): minimize imports#1455
Conversation
Co-authored-by: Claude <noreply@anthropic.com>
|
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 |
jstoobysmith
left a comment
There was a problem hiding this comment.
Thanks Alex, I've approved this one and will merge it once the Linters finish.
Summary
Minimizes the imports of
QuantumInfo/ClassicalInfo/Capacity.lean.The file only defines
Code,FixedLengthCode, andBlockCodestructures overList,Fin, andℕ— it never uses anything fromQuantumInfo.ClassicalInfo.Entropy(entropy/probability/channel definitions), nor
Fintype/Finsetinstances forFin.Replaced the three imports with the single, more basic import that the file actually
needs for its
Fin block_in/Fin block_outusage:QuantumInfo.ClassicalInfo.Entropy(unused)Mathlib.Data.Finset.Fin(unused)Mathlib.Data.Fintype.Fin(unused; replaced by the more basicMathlib.Data.Fin.Basic)Downstream impact
None.
QuantumInfo.ClassicalInfo.Capacityis not imported by any other file in therepo (its import in
QuantumInfo.leanis commented out), so no other files neededchanges.
Verification
lake build QuantumInfo.ClassicalInfo.Capacity— succeeds (510 jobs, down from 2216with the original imports)
lake build QuantumInfo— succeeds (8733 jobs)lake build Physlib— succeeds (4448 jobs)No
sorrys or axioms were added; onlyimportlines were touched.