intCoe_apply — Mathlib

English

The evaluation after coercion from ℤ to R commutes with evaluation: (f : ArithmeticFunction R) x = f x for f : ArithmeticFunction ℤ.

Русский

После приведения ℤ→R сохранение значения находится при вычислении: (f : ArithmeticFunction R) x = f x.

LaTeX

$$$(f : \\mathrm{ArithmeticFunction}(R))(x) = f(x)$$$

Lean4

@[simp]
theorem intCoe_apply [AddGroupWithOne R] {f : ArithmeticFunction ℤ} {x : ℕ} : (f : ArithmeticFunction R) x = f x :=
  rfl

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