id

Mathlib.NumberTheory.ArithmeticFunction

URI: https://scilib.ai/kg/mathlib#ArithmeticFunction.id

English

The identity on ℕ as an arithmetic function, id(n)=n.

Русский

Идентичная функция на ℕ как арифметическая функция, id(n)=n.

LaTeX

$$$\text{The identity on }\mathbb{N} \text{ as an ArithmeticFunction}$$$

Lean4

/-- The identity on `ℕ` as an `ArithmeticFunction`. -/
def id : ArithmeticFunction ℕ :=
  ⟨_root_.id, rfl⟩

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

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

Разделы

Аффилиация

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