exists_basis

Mathlib.LinearAlgebra.Basis.VectorSpace

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

English

If K and V are finite, then there exists n with |V| = |K|^n.

Русский

Если K и V конечны, то существует размерность n такая, что |V| = |K|^n.

LaTeX

$$$\exists n\in\mathbb{N}\; |V| = |K|^n$$$

Lean4

theorem exists_basis : ∃ s : Set V, Nonempty (Basis s K V) :=
  ⟨ofVectorSpaceIndex K V, ⟨ofVectorSpace K V⟩⟩

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

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

Разделы

Аффилиация

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