not_fermatLastTheoremFor_one

Mathlib.NumberTheory.FLT.Basic

URI: https://scilib.ai/kg/mathlib#not_fermatLastTheoremFor_one

English

Not (FermatLastTheoremFor 1): the theorem fails for exponent 1.

Русский

Не Ферматова теорема для n=1: теорема неверна в этом случае.

LaTeX

$$$\lnot \text{FermatLastTheoremFor}(1).$$$

Lean4

theorem not_fermatLastTheoremFor_one : ¬FermatLastTheoremFor 1 := fun h ↦
  h 1 1 2 (by simp) (by simp) (by simp) (by simp)

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru