Local fields in Lean 4

Stream: maths

[Florent Schaffhauser]

Is it ok to also post the link to the arXiv version of the article?

[Filippo A. E. Nuccio]

Here the HAL (but I think that this should be free)

[Florent Schaffhauser]

Filippo A. E. Nuccio said:

but I think that this should be free

Only the abstract and reference list (for me right now, not on a university network).

[Filippo A. E. Nuccio]

Long Live Free Repositories :smile: :free:

[Patrick Massot]

This is great! We all know it’s no fun at all to return to some job that seemed finish and fight the system to port it.

[Notification Bot]

5 messages were moved here from #announce > Local fields in Lean 4 by Johan Commelin.

[Johan Commelin]

@María Inés de Frutos Fernández @Filippo A. E. Nuccio Awesome! Great job! Looking forward to the PRs.

[Filippo A. E. Nuccio]

Johan Commelin said:

María Inés de Frutos Fernández Filippo A. E. Nuccio Awesome! Great job! Looking forward to the PRs.

Sure? We'll ping you for each of them... :wink: