instIntCast

Mathlib.Topology.LocallyConstant.Algebra

URI: https://scilib.ai/kg/mathlib#LocallyConstant.instIntCast

English

LocallyConstant X Y has an integer-cast embedding: n ↦ const_X(n).

Русский

LocallyConstant X Y имеет вложение целочисленного приведения: n ↦ константная функция n.

LaTeX

$$$\text{intCast}(n) = \text{const}_X(n).$$$

Lean4

instance [IntCast Y] : IntCast (LocallyConstant X Y) where intCast n := const X n

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru