coe_singleton

Mathlib.LinearAlgebra.Basis.Basic

URI: https://scilib.ai/kg/mathlib#Module.Basis.coe_singleton

English

The coercion of Basis.singleton is the constant-1 function on the unique index.

Русский

Переобразование Basis.singleton равно константной единице на уникальном индексе.

LaTeX

$$$\\!\\,\\ (Basis.singleton\\ ι\\ R) = 1$$$

Lean4

@[simp]
theorem coe_singleton {ι R : Type*} [Unique ι] [Semiring R] : ⇑(Basis.singleton ι R) = 1 := by ext; simp

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

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

Разделы

Аффилиация

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