finiteDimensional_quotient — Mathlib

English

Let K be a division ring, V a finite-dimensional vector space over K, and S a subspace of V. Then the quotient space V / S is finite-dimensional over K.

Русский

Пусть K — кольцо деления, V — конечномерное над K пространство, и S — подпространство V. Тогда фактор-пространство V / S конечномерно над K.

LaTeX

$$$\mathrm{FiniteDimensional}_K V \Rightarrow \mathrm{FiniteDimensional}_K (V / S)$$$

Lean4

/-- A quotient of a finite-dimensional space is also finite-dimensional. -/
instance finiteDimensional_quotient [FiniteDimensional K V] (S : Submodule K V) : FiniteDimensional K (V ⧸ S) :=
  Module.Finite.quotient K S

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