finiteDimensional_toSubmodule — Mathlib

English

A subalgebra S of E is finite-dimensional over F if and only if S, viewed as a submodule, is finite-dimensional over F.

Русский

Подалгебра S под E относительно поля F конечномерна, если и только если S как подмодуль конечномерна над F.

LaTeX

$$$\operatorname{FiniteDimensional} F (\text{Subalgebra.toSubmodule } S) \iff \operatorname{FiniteDimensional} F S$$$

Lean4

/-- A `Subalgebra` is `FiniteDimensional` iff it is `FiniteDimensional` as a submodule. -/
theorem finiteDimensional_toSubmodule {S : Subalgebra F E} :
    FiniteDimensional F (Subalgebra.toSubmodule S) ↔ FiniteDimensional F S :=
  Iff.rfl

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