instModuleDualFiniteDimensional

Mathlib.LinearAlgebra.Dual.Lemmas

URI: https://scilib.ai/kg/mathlib#Subspace.instModuleDualFiniteDimensional

English

If V is finite dimensional, then its dual space V* is also finite dimensional.

Русский

Если V конечномерно, то и его двойственное пространство V* тоже конечномерно.

LaTeX

$$FiniteDimensional K V ⇒ FiniteDimensional K (Module.Dual K V)$$

Lean4

instance instModuleDualFiniteDimensional [FiniteDimensional K V] : FiniteDimensional K (Module.Dual K V) := by
  infer_instance

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

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

Разделы

Аффилиация

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