Fermat Last Theorem

Stream: FLT

[Kevin Buzzard]

OK so I am close to having some preliminary Lean/LaTeX/blueprint ready for a formal opening of the FLT repo. This has involved writing some code which refers to docs#FermatLastTheorem a lot. Note "Fermat", not "Fermat's". I've written "FermatLastTheorem" quite a bit now and it still sounds really odd to me. This change was added to my FLT mathlib PR by Yael here at the same time as another change, and I didn't notice this until the PR was merged.

I propose changing FermatLast to FermatsLast throughout that mathlib file. Are there reasons why I shouldn't do this, e.g. to do with the naming convention? My argument for the change is simply "Fermat's Last Theorem is what everyone calls it in English".

[Chris Birkbeck]

I agree that it should be FermatsLast.

[Joseph Myers]

Lean supports ' in identifiers, why not Fermat'sLastTheorem?

[Kevin Buzzard]

I would also be happy with that!

[David Michael Roberts]

Ferma'sLastTheorem, even :zany_face:

[Utensil Song]

In PFR, having ' in the theorem name broke the whole dep graph in the blueprint, but it's fixed now.

[David Renshaw]

def «Fermat's Last Theorem» ...