coe_coe — Mathlib

English

Coercing ℕ-valued arithmetic functions through ℤ to R is the same as direct coercion to R; i.e., ((f : ArithmeticFunction ℤ) : ArithmeticFunction R) = (f : ArithmeticFunction R).

Русский

Приведение арифметической функции ℕ сначала через ℤ, затем в R равно прямому привидению к R.

LaTeX

$$$((f : \\mathrm{ArithmeticFunction}(\\mathbb{Z})) : \\mathrm{ArithmeticFunction}(R)) = (f : \\mathrm{ArithmeticFunction}(R))$ for all $f : \\mathrm{ArithmeticFunction}(\\mathbb{N})$$$

Lean4

@[simp]
theorem coe_coe [AddGroupWithOne R] {f : ArithmeticFunction ℕ} :
    ((f : ArithmeticFunction ℤ) : ArithmeticFunction R) = (f : ArithmeticFunction R) :=
  by
  ext
  simp

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