Bryan Gin-ge Chen

icon location here to learn

Results 105 comments of Bryan Gin-ge Chen

Add more exceptions to the naming rules to adhere with the current conventions

> I agree, and I am willing to contribute a bit. Do you know if the link https://leanprover-community.github.io/ci.html that appears in the middle of the page has been moved, deleted,...

Add more exceptions to the naming rules to adhere with the current conventions

Ah, I see. Yes, it would be good to at least link to the wiki or maybe copy / move the most useful instructions there.

Support Lean 3.15.0 (including widgets)

The relevant PR is https://github.com/leanprover-community/lean/pull/258. I think you can ping @EdAyers if you have any questions.

Naming conventions doc has significant amount of duplicated text

The new location is https://github.com/leanprover-community/leanprover-community.github.io/blob/3a6244b3b59d42a02316ef23ea7d7f646aebe491/templates/contribute/naming.md

I hope this paragraph about `leanpkg` and `leanproject` can be made easier to find

It's true that it's not versioned separately from `lean` itself. But you can check `lean --version`. You can also see all commits changing `leanpkg` [here](https://github.com/leanprover-community/lean/commits/master/leanpkg) or you can search the...

feat(NumberField/CanonicalEmbedding): Define the fundamental cone for the action of the units of a number field

This one seems to have fallen off the queue when bors crashed (not your fault). bors r+ Just in case something happens again: bors d+

feat(Fin/Parity): add `Fin.even_iff`

bors d=IvanRenison

feat(Fin/Parity): add `Fin.even_iff`

Please merge `master`, fix the breakage and then merge with `bors d+` when done, thanks!

Type vars in `data/polynomial/splitting_field`

We don't have a `data/polynomial/splitting_field.lean` (anymore?). Is the issue about code in `field_theory/splitting_field.lean`?

1000.html: link IDs to their wikidata page

Nice idea! Could you add similar code to `1000-missing.html` for completeness?