intCoe_int

Mathlib.NumberTheory.ArithmeticFunction

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

English

For any f : ArithmeticFunction ℤ, applying ofInt to f yields f itself; i.e., ofInt f = f.

Русский

Для любой f : ArithmeticFunction ℤ преобразование ofInt возвращает саму f, то есть ofInt f = f.

LaTeX

$$$\\operatorname{ofInt} f = f$ for all $f:\\mathrm{ArithmeticFunction}(\\mathbb{Z})$$$

Lean4

@[simp]
theorem intCoe_int (f : ArithmeticFunction ℤ) : ofInt f = f :=
  ext fun _ => Int.cast_id

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

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

Разделы

Аффилиация

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