1d971c8735
This PR implements the Rabinowitsch transformation for `Field` disequalities in `grind`. For example, this transformation is necessary for solving: ```lean example [Field α] (a : α) : a^2 = 0 → a = 0 := by grind ``` |
||
|---|---|---|
| .. | ||
| bench | ||
| compiler | ||
| elabissues | ||
| ir | ||
| lean | ||
| pkg | ||
| playground | ||
| plugin | ||
| simpperf | ||
| .gitignore | ||
| common.sh | ||
| lean-toolchain | ||