Alex J Best
Alex J Best
It would be great if this tool could be used to find circular dependencies in [cython](http://cython.org/) projects also. Cython syntax is a lot more involved in general, but the import...
I had a go at Minkowski's convex body theorem and it works thanks to @urkud 's pidgeonhole for measurable spaces. My interest is in the applications to number theory, hence...
### Checklist - [X] I added a descriptive title - [X] I searched open requests and couldn't find a duplicate ### What is the idea? It would be useful to...
I have some code that makes use of unicode greek letters for variables (nu, lambda, kappa, mu) (thanks python3!) that I'm trying to include in a pretext program. However the...
As reported by @b-mehta on Zulip in https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/.60open.20finset.60.20changes.20truth.20of.20goal/near/304982461 it is possible that simply opening a namespace which contains overloaded function names can cause the argument types to be elaborated differently,...
Currently we see the following error in Sage ```sage sage: R. = QQ[] sage: K = NumberField(y^2-y-1,'a') sage: A = pari(K).alginit([2,[[],[]],[0,0]]) sage: K(A.algb()) 1 sage: K(A.algb()) --------------------------------------------------------------------------- SystemError Traceback (most...
In mathlib (3) we had a syntax for citing references stored in a `.bib` file and displaying them in a custom page https://leanprover-community.github.io/mathlib_docs/references.html. We previously used the `pybtex` python library...