_example

Mathlib.NumberTheory.FLT.Three

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

English

If p divides both S.a + S.b and S.a + η S.b, then p is associated with λ.

Русский

Если p делит S.a + S.b и S.a + η S.b, то p ассоциировано с λ.

LaTeX

$$Associated p λ$$

Lean4

example (a b : 𝓞 K) (ha : a ≠ 0) (hb : b ≠ 0) : a * b ≠ 0 := by exact mul_ne_zero ha hb

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

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

Разделы

Аффилиация

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