fermatLastTheoremWith' — Mathlib

English

If FermatLastTheoremWith R n holds, then FermatLastTheoremWith' R n holds as well; the former implies the latter.

Русский

Если FermatLastTheoremWith R n выполняется, то FermatLastTheoremWith' R n тоже выполняется; первый следовательно второй.

LaTeX

$$$FermatLastTheoremWith\\ R\\ n \\rightarrow FermatLastTheoremWith'\\ R\\ n$$$

Lean4

theorem fermatLastTheoremWith' {R : Type*} [CommSemiring R] {n : ℕ} (h : FermatLastTheoremWith R n) :
    FermatLastTheoremWith' R n := fun a b c _ _ _ _ ↦ by exfalso; apply h a b c <;> assumption

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