range_ofVectorSpace

Mathlib.LinearAlgebra.Basis.VectorSpace

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

English

There exists a basis for every vector space.

Русский

У каждого векторного пространства существует базис.

LaTeX

$$$\exists B\,\text{basis of } V$$$

Lean4

theorem range_ofVectorSpace : range (ofVectorSpace K V) = ofVectorSpaceIndex K V :=
  range_extend _

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

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

Разделы

Аффилиация

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