Skip to content

Commit

Permalink
chore(linarith): remove unused import (#13745)
Browse files Browse the repository at this point in the history
  • Loading branch information
kim-em authored and AntoineChambert-Loir committed Jun 20, 2024
1 parent 52ecd68 commit d113283
Showing 1 changed file with 0 additions and 1 deletion.
1 change: 0 additions & 1 deletion Mathlib/Tactic/Linarith/Frontend.lean
Original file line number Diff line number Diff line change
Expand Up @@ -4,7 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
Authors: Robert Y. Lewis
-/
import Mathlib.Control.Basic
import Mathlib.Data.HashMap
import Mathlib.Tactic.Linarith.Verification
import Mathlib.Tactic.Linarith.Preprocessing

Expand Down

0 comments on commit d113283

Please sign in to comment.