finiteDimensional_subalgebra — Mathlib

English

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

Русский

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

LaTeX

$$$\text{FiniteDimensional } F E \Rightarrow \text{FiniteDimensional } F S$$$

Lean4

instance finiteDimensional_subalgebra [FiniteDimensional F E] (S : Subalgebra F E) : FiniteDimensional F S :=
  FiniteDimensional.of_subalgebra_toSubmodule inferInstance

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