fermatLastTheoremFor_iff_int

Mathlib.NumberTheory.FLT.Basic

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

← MathLib Explorer

English

FermatLastTheoremFor n is equivalent to FermatLastTheoremWith ℤ n.

Русский

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

LaTeX

$$$FermatLastTheoremFor\\ n \\iff FermatLastTheoremWith\\ ℤ\\ n$$$

Lean4

theorem fermatLastTheoremFor_iff_int {n : ℕ} : FermatLastTheoremFor n ↔ FermatLastTheoremWith ℤ n :=
  (fermatLastTheoremWith_nat_int_rat_tfae n).out 0 1

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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