fermatLastTheoremWith'_iff_fermatLastTheoremWith

English

Assume a no-unit-solution condition hn; then FermatLastTheoremWith' R n is equivalent to FermatLastTheoremWith R n.

Русский

При условии отсутствия единичных решений для уравнения a^n + b^n = c^n, тождество FermatLastTheoremWith' R n эквивалентно FermatLastTheoremWith R n.

LaTeX

$$$\\forall R\\ [CommSemiring R] [IsDomain R] {n},\\ (\\forall a,b,c \\in R, IsUnit a \\to IsUnit b \\to IsUnit c \\to a^n + b^n \\neq c^n) \\rightarrow (FermatLastTheoremWith' R n) \\,\\leftrightarrow \\, FermatLastTheoremWith R n$$$

Lean4

theorem fermatLastTheoremWith'_iff_fermatLastTheoremWith {R : Type*} [CommSemiring R] [IsDomain R] {n : ℕ}
    (hn : ∀ a b c : R, IsUnit a → IsUnit b → IsUnit c → a ^ n + b ^ n ≠ c ^ n) :
    FermatLastTheoremWith' R n ↔ FermatLastTheoremWith R n :=
  Iff.intro (fun h ↦ h.fermatLastTheoremWith hn) (fun h ↦ h.fermatLastTheoremWith')

Похожие утверждения