greg/NNG
1
0
Fork 0
Code Issues Pull Requests Actions Packages Projects Releases Wiki Activity

remove ring tactic

Browse Source
This commit is contained in:
Jon Eugster
2024-03-14 11:13:59 +01:00
parent d6bf5686bc
commit 5010691770
1 changed files with 1 additions and 2 deletions
Download Patch File Download Diff File Expand all files Collapse all files

3
Game/Tactic/FromMathlib.lean
View File

@@ -1,7 +1,6 @@
import Mathlib.Tactic.NthRewrite
import Mathlib.Tactic.Tauto
import Mathlib.Tactic.Ring -- this is bad because it adds `mul_comm` to the `_root_` namespace, interfering with `MyNat.mul_comm`.
-- import Mathlib.Tactic.Ring -- this is bad because it adds `mul_comm` to the `_root_` namespace, interfering with `MyNat.mul_comm`.
-- import Mathlib.Tactic.Abel
-- import Mathlib.Tactic.ApplyAt