Skip to content

Commit

Permalink
Fix import issue
Browse files Browse the repository at this point in the history
  • Loading branch information
@Paul-Lez
Paul-Lez committed Nov 30, 2024
1 parent 98c7a83 commit 05f1ecf
Showing 1 changed file with 2 additions and 2 deletions.
4 changes: 2 additions & 2 deletions PersistentDecomp.lean
View file
Original file line number Diff line number Diff line change
Expand Up @@ -8,5 +8,5 @@ import PersistentDecomp.Mathlib.Order.Interval.Basic
import PersistentDecomp.Mathlib.Order.SupIndep
import PersistentDecomp.Prereqs.Indecomposable
import PersistentDecomp.Prereqs.PersistenceSubmodule
import PersistentDecomp.step_2
import PersistentDecomp.thm1_1
import PersistentDecomp.EndoRingIsLocal
import PersistentDecomp.MaximalDecompExists

0 comments on commit 05f1ecf

Please sign in to comment.