coe_basisSingleOne

Mathlib.LinearAlgebra.Finsupp.VectorSpace

URI: https://scilib.ai/kg/mathlib#Finsupp.coe_basisSingleOne

← MathLib Explorer

English

The canonical coe of the BasisSingleOne basis equals the map i ↦ single i 1.

Русский

Каноническое отображение BasisSingleOne соответствует отображению i ↦ single i 1.

LaTeX

$$$\\text{BasisSingleOne}.coe = \\lambda i. \\mathrm{single}_i(1)$$$

Lean4

@[simp]
theorem coe_basisSingleOne : (Finsupp.basisSingleOne : ι → ι →₀ R) = fun i => Finsupp.single i 1 :=
  funext fun _ => Basis.apply_eq_iff.mpr rfl

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

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

Разделы

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

Аффилиация

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