We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
1 parent 49079cb commit bef29e2Copy full SHA for bef29e2
Katydid/Example/SimpLibrary.lean
@@ -1,4 +1,4 @@
1
--- Examlpe of how to use @[simp] to include theorems in simp
+-- Example of how to use @[simp] to include theorems in simp
2
-- see https://github.com/leanprover-community/mathlib4/blob/56c1ca9832bdd85620d6b0bbd37ef56818e6b667/Mathlib/Data/Matrix/Basis.lean
3
4
namespace SimpLibrary
0 commit comments