instInhabitedArithmeticFunction

Mathlib.NumberTheory.ArithmeticFunction

URI: https://scilib.ai/kg/mathlib#instInhabitedArithmeticFunction

English

The function (1) defined on inputs gives 1 at input x=1 and 0 otherwise.

Русский

Функция (1) при вводе x даёт 1 при x=1 и 0 при x≠1.

LaTeX

$$$(1 : ArithmeticFunction R)(x) = \\begin{cases}1,& x=1 \\\\ 0,& x\\neq 1\\end{cases}$$$

Lean4

instance [Zero R] : Inhabited (ArithmeticFunction R) :=
  inferInstanceAs (Inhabited (ZeroHom ℕ R))

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

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

Разделы

Аффилиация

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