English
Mason–Stothers (polynomial ABC) theorem: for coprime polynomials a,b,c with a+b+c=0, degrees are bounded by the radical of abc or all derivatives vanish.
Русский
Теорема Майсона–Стотерса в полиномах: для взаимно простых полиномов a,b,c с a+b+c=0, степени удовлетворяют указанному неравенству или все производные обращаются в ноль.
LaTeX
$$$\text{IsCoprime } a b \Rightarrow (a+b+c)=0 \Rightarrow \Big(\big(\deg a+1 \le \deg \operatorname{rad}(abc)\big)\land\cdots\Big) \;\lor\; (a',b',c'\text{ all derivatives }=0).$$$
Lean4
/-- Fermat's Last Theorem for $n=4$: if `a b c : ℕ` are all non-zero
then `a ^ 4 + b ^ 4 ≠ c ^ 4`.
-/
theorem fermatLastTheoremFour : FermatLastTheoremFor 4 :=
by
rw [fermatLastTheoremFor_iff_int]
intro a b c ha hb _ heq
apply @not_fermat_42 _ _ (c ^ 2) ha hb
rw [heq]; ring
