I have two interns from École Polytechnique. They have been going over
HOL-Algebra and Group-Ring-Module, providing new proofs of the best results in
the latter and tidying up some messy proofs in the former, as well. They are
also systematising the chaotic naming conventions that they found the
I have a student who was going to formalise things about fields and
field extensions. Does that clash with your work in any way?
In any case, we should definitely coordinate our efforts here to avoid
duplication of work.
Manuel
On 2018-05-08 13:49, Lawrence Paulson wrote:
> I have two interns f
