intCoe_one — Mathlib

English

Similarly, embedding the constant function 1 from ℤ into R yields the constant function 1 in R.

Русский

Аналогично, константа 1 из ℤ при приведении в R даёт константу 1.

LaTeX

$$$((1:\\mathrm{ArithmeticFunction}(\\mathbb{Z})) : \\mathrm{ArithmeticFunction}(R)) = 1$$$

Lean4

@[simp]
theorem intCoe_one [AddGroupWithOne R] : ((1 : ArithmeticFunction ℤ) : ArithmeticFunction R) = 1 :=
  by
  ext n
  simp [one_apply]

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