coe_ofVectorSpace

Mathlib.LinearAlgebra.Basis.VectorSpace

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

English

The underlying function of Basis.ofVectorSpace is the inclusion into V.

Русский

Функция Basis.ofVectorSpace является включением в V.

LaTeX

$$$\text{coe\_ofVectorSpace} : (\mathrm{Basis.ofVectorSpace}(K,V)) = \iota$$$

Lean4

@[simp]
theorem coe_ofVectorSpace : ⇑(ofVectorSpace K V) = ((↑) : _ → _) :=
  funext fun x => ofVectorSpace_apply_self K V x

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

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

Разделы

Аффилиация

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