Johan Commelin

co-authored-by: github username

4

Thanks for bors! I love it. Would it be possible to support github usernames in `co-authored-by:` lines? (In addition to "N. Ame ") ``` Co-authored-by: @jcommelin ``` Often I know...

refactor(tactic/wlog): simplify and speed up `wlog`

25

Benefits: - The tactic is faster - The tactic is easier to port to Lean 4 Downside: - The tactic doesn't do any heavy-lifting for the user Zulip thread: https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/wlog/near/296996966...

Bug in widgets: type of `i` in `∃ i, ...` is wrong

2

### Description In the widget view, if you hover over the `i` in `∃ i, ...` it doesn't show the type of `i`, but the type of the lambda that...

race condition when PRs are closed (almost) simultaneously

2

Over at leanprover-community/mathlib we use the `bors` bot (bors-ng) to merge PRs for us. (CI takes > 1 hour, and we have 10 - 20 PRs per day, so we...

Support for drafts

1

Is it an option to factor out the part of the script that removes the `Notmuch-Help` lines and parses the `Attach:` lines, so that one can save a draft and...

### Describe the bug In mathematics, it is common to denote the ring of formal power series using double square brackets, for example: `$\mathbb C[[t]]$` Writing this in a Foam...

Jordan normal form

2

https://en.wikipedia.org/wiki/Jordan_normal_form

feat(ring_theory/mv_polynomial/symmetric): Symmetric polynomials

1

Define several kinds of symmetric polynomials. ---