of_fact_finrank_eq_two — Mathlib

English

If a division ring K and a K-vector space V have finite dimension 2, then V is finite-dimensional over K.

Русский

Если кольцо деления K и пространство V над K имеют размерность 2, то V конечно размерно над K.

LaTeX

$$FiniteDimensional K V$$

Lean4

theorem of_fact_finrank_eq_two {K V : Type*} [DivisionRing K] [AddCommGroup V] [Module K V] [Fact (finrank K V = 2)] :
    FiniteDimensional K V :=
  .of_fact_finrank_eq_succ 1

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