one_apply_ne

Mathlib.NumberTheory.ArithmeticFunction

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

English

If x ≠ 1, then the unit function evaluates to 0 at x.

Русский

Если x ≠ 1, единичная функция принимает значение 0 в x.

LaTeX

$$$\\forall x \\neq 1, (1 : ArithmeticFunction R) x = 0$$$

Lean4

@[simp]
theorem one_apply_ne {x : ℕ} (h : x ≠ 1) : (1 : ArithmeticFunction R) x = 0 :=
  if_neg h

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

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

Разделы

Аффилиация

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