finiteDimensional_submodule — Mathlib

English

If E is a finite-dimensional algebra over F, then any subalgebra S of E is finite-dimensional over F.

Русский

Если E является конечномерной алгеброй над F, то любая подалгебра S внутри E конечномерна над F.

LaTeX

$$FiniteDimensional F E ⇒ [FiniteDimensional F S] for S : Subalgebra F E$$

Lean4

/-- A subspace of a finite-dimensional space is also finite-dimensional.

This is a shortcut instance to simplify inference in the presence of `[FiniteDimensional K V]`.
-/
instance finiteDimensional_submodule [FiniteDimensional K V] (S : Submodule K V) : FiniteDimensional K S := by
  infer_instance

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