fermatLastTheoremFor_iff_nat

Mathlib.NumberTheory.FLT.Basic

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

English

FermatLastTheoremFor n is equivalent to FermatLastTheoremWith Nat n.

Русский

FermatLastTheoremFor n эквивалентна FermatLastTheoremWith Nat n.

LaTeX

$$$FermatLastTheoremFor\\ n \\iff FermatLastTheoremWith\\Nat\\ n$$$

Lean4

theorem fermatLastTheoremFor_iff_nat {n : ℕ} : FermatLastTheoremFor n ↔ FermatLastTheoremWith ℕ n :=
  Iff.rfl

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

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

Разделы

Аффилиация

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