Fermat's Last Theorem for exponent 11

The theorem asserts FermatLastTheoremFor 11, i.e. the Mathlib predicate stating that for all natural numbers $a$, $b$, $c$ with $a \neq 0$, $b \neq 0$ and $c \neq 0$ one has $a^{11} + b^{11} \neq c^{11}$. There are no parameters and no hypotheses: this is a closed statement about the exponent $11$ only, phrased entirely in Mathlib terms (no project-specific notion occurs in it). Note that, as with Mathlib's FermatLastTheoremFor, the quantification is over natural numbers with all three variables nonzero; the equivalent formulations over the integers or over nonzero rationals are not what is literally asserted here, though they are standard consequences. In particular nothing about the cases $a^{11}+b^{11}=c^{11}$ with one of the variables zero, or about other exponents, is claimed.

This is Fermat's Last Theorem for the regular prime exponent $11$, in the form going back to Kummer's treatment of regular primes; the formal statement is the Mathlib predicate for a single exponent rather than the general theorem, and the input "$11$ is regular" is here supplied in the sharper shape $h(\mathbb{Q}(\zeta_{11})) = 1$. Within the project it is used to dispose of the exponent $11$ in the Frey-package analysis: FreyPackage.frey_no_cofixed_eleven appeals to it when the Frey package's exponent is $11$, the hypotheses of such a package then being contradictory.