not_fermatLastTheoremFor_two

Mathlib.NumberTheory.FLT.Basic

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

English

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

Русский

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

LaTeX

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

Lean4

theorem not_fermatLastTheoremFor_two : ¬FermatLastTheoremFor 2 := fun h ↦
  h 3 4 5 (by simp) (by simp) (by simp) (by simp)

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

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

Разделы

Аффилиация

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