Commit 2022-12-06 23:13 213105f2

View on Github →

fix: removed (incorrect) test for symm, trans attributes (#857) Fixes error I made: introducing a test for symm and trans attributes to check that the lemmas were "genuinely" symm/trans lemmas. However the tests had false positives, e.g. #855 (which has been added to the tests). This short commit removes the tests. They were not present in mathlib3 anyway and the worst that happens if a lemma is incorrectly labelled is that the symm tactic tries and fails with this. As a warning it may be useful to have a test, but it should have no false positives. For now it seems the best approach is to drop the test.

Estimated changes

added structure MulEquiv
added def MulHom.inverse
added def foo_symm