Skip to content

Commit 135bfc5

Browse files
committed
Min imports
1 parent ba3c5c1 commit 135bfc5

1 file changed

Lines changed: 4 additions & 2 deletions

File tree

ArkLib/Data/CodingTheory/ProximityGap/Folding/FoldingContext.lean

Lines changed: 4 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -4,8 +4,10 @@ Released under Apache 2.0 license as described in the file LICENSE.
44
Authors: František Silváši, Ilia Vlasov, Aristotle (Harmonic)
55
-/
66

7-
import Mathlib.Data.Nat.Basic
8-
import ArkLib.Data.Fin.Basic
7+
import Mathlib.Algebra.Order.Group.Nat
8+
import Mathlib.Algebra.Order.Monoid.Unbundled.Pow
9+
import Mathlib.Data.Nat.Cast.Order.Basic
10+
import Mathlib.Order.Lattice.Nat
911

1012
/-! # The folding context
1113

0 commit comments

Comments
 (0)