fermatLastTheoremFor_iff_rat

Mathlib.NumberTheory.FLT.Basic

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

← MathLib Explorer

English

FermatLastTheoremFor n is equivalent to FermatLastTheoremWith ℚ n.

Русский

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

LaTeX

$$$FermatLastTheoremFor\\ n \\iff FermatLastTheoremWith\\ Rat\\ n$$$

Lean4

theorem fermatLastTheoremFor_iff_rat {n : ℕ} : FermatLastTheoremFor n ↔ FermatLastTheoremWith ℚ n :=
  (fermatLastTheoremWith_nat_int_rat_tfae n).out 0 2

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

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

Разделы

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

Аффилиация

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