totient_one

Mathlib.Data.Nat.Totient

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

English

For n = 1, the totient φ(1) equals 1.

Русский

Для n = 1 функция Эйлера даёт φ(1) = 1.

LaTeX

$$$$\varphi(1) = 1.$$$$

Lean4

@[simp]
theorem totient_one : φ 1 = 1 :=
  rfl

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

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

Разделы

Аффилиация

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