isClassified_of_isPrimitiveClassified

Mathlib.NumberTheory.PythagoreanTriples

URI: https://scilib.ai/kg/mathlib#PythagoreanTriple.isClassified_of_isPrimitiveClassified

English

If h.IsPrimitiveClassified, then h.IsClassified.

Русский

Если тройка примитивно классифицирована, то она классифицирована.

LaTeX

$$$h.IsPrimitiveClassified \Rightarrow h.IsClassified$$$

Lean4

theorem isClassified_of_isPrimitiveClassified (hp : h.IsPrimitiveClassified) : h.IsClassified :=
  by
  obtain ⟨m, n, H⟩ := hp
  use 1, m, n
  cutsat

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

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

Разделы

Аффилиация

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