English
Let R be a commutative semiring with no zero divisors. For natural numbers m and n, if m divides n and Fermat Last Theorem holds for exponent m over R, then Fermat Last Theorem holds for exponent n over R.
Русский
Пусть R — коммутативное полукольцо без нулевых делителей. Пусть m, n ∈ ℕ, и m делит n. Если теорема Ферма верна для показателя m над R, то она верна и для показателя n над R.
LaTeX
$$$\\forall R\\, [\\text{Semiring } R]\\, [\\text{NoZeroDivisors } R]\,\\, \\forall m,n\\in \\mathbb{N},\\ m \\mid n \\rightarrow (FermatLastTheoremWith\\ R\\ m \\rightarrow FermatLastTheoremWith\\ R\\ n)$$$
Lean4
theorem mono (hmn : m ∣ n) (hm : FermatLastTheoremWith R m) : FermatLastTheoremWith R n :=
by
rintro a b c ha hb hc
obtain ⟨k, rfl⟩ := hmn
simp_rw [pow_mul']
refine hm _ _ _ ?_ ?_ ?_ <;> exact pow_ne_zero _ ‹_›
