basic): delete `import tactic.linarith` (#15075)

Commit

3 years ago

chore(data/nat/factorization/basic): delete `import tactic.linarith` (#15075) Removes the import of `tactic.linarith` that's no longer needed.

Author

stuart-presnell

Parents