singleton_repr

Mathlib.LinearAlgebra.Basis.Basic

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

← MathLib Explorer

English

The singleton basis has the property that its repr at x and index i equals x for the unique i.

Русский

У базиса singleton выполняется, что его repr x по уникальному индексу равен x.

LaTeX

$$$(Basis.singleton\\ ι\\ R).repr\\ x\\ i = x$$$

Lean4

@[simp]
theorem singleton_repr (ι R : Type*) [Unique ι] [Semiring R] (x i) : (Basis.singleton ι R).repr x i = x := by
  simp [Basis.singleton, Unique.eq_default i]

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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