intCast_def — Mathlib

English

For any integer n, the germ of the constant function sending every input to n equals n in Germ_l M.

Русский

Для любого целого числа n жерма константной функции, отправляющей каждый вход в n, равна n в Germ_l M.

LaTeX

$$$[IntCast\\ M] (n : \\mathbb{Z}) : ((fun _ \\mapsto n : \\alpha \\to M) : Germ\\ l\\ M) = n.$$$

Lean4

@[simp]
theorem intCast_def [IntCast M] (n : ℤ) : ((fun _ ↦ n : α → M) : Germ l M) = n :=
  rfl

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