two_le_multiplicity

Mathlib.NumberTheory.FLT.Three

URI: https://scilib.ai/kg/mathlib#FermatLastTheoremForThreeGen.Solution.two_le_multiplicity

← MathLib Explorer

English

Another formulation that two is less-or-equal multiplicity of a certain object.

Русский

Еще одно формулирование: две кратности меньшие или равны определенному объекту.

LaTeX

$$$2 \le S'.multiplicity$$$

Lean4

/-- Given `S : Solution`, we have that `2 ≤ S.multiplicity`. -/
theorem two_le_multiplicity : 2 ≤ S.multiplicity :=
  S.toSolution'.two_le_multiplicity

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

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

Разделы

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

Аффилиация

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