coe_intCast — Mathlib

English

Integers embed into SimpleFunc via constant functions: the nth integer is the constant function with value n.

Русский

Целые числа инкорпорируются в SimpleFunc через константные функции: n-й целый — константа n.

LaTeX

$$$\\text{coe\_intCast } [IntCast \\beta] (n: \\mathbb{Z}) : \\; \\⇑(↑n : \\alpha \\to_{S} \\beta) = \\text{fun } _ \\mapsto n.$$$

Lean4

@[simp, norm_cast]
theorem coe_intCast [IntCast β] (n : ℤ) : ⇑(↑n : α →ₛ β) = fun _ ↦ ↑n :=
  rfl

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