Adds a variant FermatLastTheoremWith' of FLT for general commutative semirings, allowing nonzero unit solutions and their multiples.

Supersedes #14270. I find this version less intrusive to the original statement of FLT.

The relaxed 'unit' variant FermatLastTheoremWith' α states that any nonzero solution to Fermat equation $a^n+b^n=c^n$ should be units $(a, b, c)$ or their common multiples. The stronger original FermatLastTheoremWith α states that there is no nonzero solution $(a, b, c)$ from the beginning.

For α = ℕ or ℤ the two statements are equivalent to the original FLT. A purpose of this is to include a polynomial version of FLT which is easy to prove (relevant Zulip discussion here). FermatLastTheoremWith k[X] is false for general field $k$, but FermatLastTheoremWith' k[X] is.

I speculate that for some integral ring α over ℤ, the original statement of FLT is false while the suggested unit variant is true. For example, take the integral closure of $\mathbb{Z}[w]$ where $w = (-1 + \sqrt{3} i ) / 2$ is the 3rd root of unity satisfying $w^3 = 1$. The original statement for $n = 6k + 1$ is false as $w^n + (w^2)^n = (-1)^n$, but note that the solutions only consists of units.