From beb9e1ad236d56738a63d385e71ccb8987507175 Mon Sep 17 00:00:00 2001 From: Alex-Zughaid <117576511+Alex-Zughaid@users.noreply.github.com> Date: Wed, 22 Jul 2026 10:01:02 +0100 Subject: [PATCH] auto-task(QuantumInfo.ClassicalInfo.Capacity): minimize imports Co-authored-by: Claude --- QuantumInfo/ClassicalInfo/Capacity.lean | 4 +--- 1 file changed, 1 insertion(+), 3 deletions(-) diff --git a/QuantumInfo/ClassicalInfo/Capacity.lean b/QuantumInfo/ClassicalInfo/Capacity.lean index 8722232a1..6f6c26e10 100644 --- a/QuantumInfo/ClassicalInfo/Capacity.lean +++ b/QuantumInfo/ClassicalInfo/Capacity.lean @@ -5,9 +5,7 @@ Authors: Alex Meiburg -/ module -public import QuantumInfo.ClassicalInfo.Entropy -public import Mathlib.Data.Finset.Fin -public import Mathlib.Data.Fintype.Fin +public import Mathlib.Data.Fin.Basic @[expose] public section