dvd_two_of_totient_le_one

Mathlib.Data.Nat.Totient

URI: https://scilib.ai/kg/mathlib#Nat.dvd_two_of_totient_le_one

← MathLib Explorer

English

If a > 0 and φ(a) ≤ 1, then a divides 2.

Русский

Если a > 0 и φ(a) ≤ 1, то a делит 2.

LaTeX

$$$$ \forall a \in \\mathbb{N}, \\, (0 < a \\\\land \\\\varphi(a) \\\\le 1) \\\\rightarrow a \\\\\\mid 2 $$$$

Lean4

theorem dvd_two_of_totient_le_one {a : ℕ} (han : 0 < a) (ha : a.totient ≤ 1) : a ∣ 2 := by
  rcases totient_eq_one_iff.mp <| le_antisymm ha <| totient_pos.2 han with rfl | rfl <;> norm_num

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

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

Разделы

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

Аффилиация

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