FermatLastTheoremWith — Mathlib

English

Fermat's Last Theorem with exponent n over a given semiring R states that for all a,b,c ∈ R with a ≠ 0, b ≠ 0, c ≠ 0, a^n + b^n ≠ c^n.

Русский

Теорема Ферма для произвольного полуправильного кольца (полуколичества) с показателем n, утверждает, что не существует ненулевых a,b,c ∈ R таких, что a^n + b^n = c^n.

LaTeX

$$$\text{FermatLastTheoremWith}(R, n) \equiv \forall a,b,c\in R, a\neq 0\to b\neq 0\to c\neq 0\to a^n + b^n \neq c^n.$$$

Lean4

/-- Statement of Fermat's Last Theorem over a given semiring with a specific exponent. -/
def FermatLastTheoremWith (R : Type*) [Semiring R] (n : ℕ) : Prop :=
  ∀ a b c : R, a ≠ 0 → b ≠ 0 → c ≠ 0 → a ^ n + b ^ n ≠ c ^ n

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