finrank_of_infinite_dimensional

Mathlib.LinearAlgebra.FiniteDimensional.Defs

URI: https://scilib.ai/kg/mathlib#Module.finrank_of_infinite_dimensional

English

If a space is not finite-dimensional, then its finrank is zero.

Русский

Если пространство не конечномерно, то его финранк равен нулю.

LaTeX

$$Not (FiniteDimensional K V) ⇒ finrank K V = 0$$

Lean4

theorem finrank_of_infinite_dimensional (h : ¬FiniteDimensional K V) : finrank K V = 0 :=
  Module.finrank_of_not_finite h

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

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

Разделы

Аффилиация

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