totient_zero

Mathlib.Data.Nat.Totient

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

English

For n = 0, the totient equals 0. That is, φ(0) = 0.

Русский

Для n = 0 смысловая единица: φ(0) = 0.

LaTeX

$$$$\varphi(0) = 0.$$$$

Lean4

@[simp]
theorem totient_zero : φ 0 = 0 :=
  rfl

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

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

Разделы

Аффилиация

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