Anne Baanen
Anne Baanen
### Prerequisites * [x] Put an X between the brackets on this line if you have done all of the following: * Checked that your issue isn't already [filed](https://github.com/leanprover-community/lean/issues). *...
### Prerequisites * [x] Put an X between the brackets on this line if you have done all of the following: * Checked that your issue isn't already [filed](https://github.com/leanprover-community/lean/issues). *...
Local variables appearing on the last line of a `do` block inside tactic mode cause an incorrect "unknown identifier" error: ```lean example (foo bar : list ℤ) : false :=...
This PR extends the `ring` tactic with a new config argument `char` which will try to reduce all constant terms modulo the given characteristic. This allows `ring` to prove e.g....
The lemma `normalize_apply` feels to me like it exposes the implementation detail that `normalize` is defined in terms of `normUnit`. I think the `normalize` function itself is much more familiar...
The `shake` command doesn't depend on Mathlib so let's upstream it and make it available for other projects. This version still has some settings hardcoded to use Mathlib as default....
There were still a few references to Mathlib in Shake, in particular it had Mathlib hardcoded as the default module to shake. Instead ask Lake what the default targets are....
This PR adds a file with support for [Lean](https://lean-lang.org) error message syntax. We use the `problem-matcher-wrap` action in CI for projects in the Lean language, especially https://github.com/leanprover-community/mathlib4. [Lean changed its...
We are missing instances `add_submonoid_class S M → has_coe S (add_submonoid M)` (probably `has_coe_t` now that I think of it), so we can just use `coe` [here](https://github.com/leanprover-community/mathlib/pull/14583#discussion_r907373588_). Similar coercions should...
In the later PRs (#4297, #4430) for this series of definitions, I had suggestions that would apply equally to the previous files in the series (#4077, #4079, #4041). These should...