Skip to content
This repository has been archived by the owner on Jul 24, 2024. It is now read-only.

Commit

Permalink
chore(tactic/default): import linear_combination (#11942)
Browse files Browse the repository at this point in the history
  • Loading branch information
robertylewis committed Feb 10, 2022
1 parent ea0e458 commit e9a1893
Showing 1 changed file with 1 addition and 0 deletions.
1 change: 1 addition & 0 deletions src/tactic/default.lean
Original file line number Diff line number Diff line change
Expand Up @@ -36,3 +36,4 @@ import tactic.zify
import tactic.transport
import tactic.unfold_cases
import tactic.field_simp
import tactic.linear_combination

0 comments on commit e9a1893

Please sign in to comment.