of_divisionRing — Mathlib

English

A vector space over a division ring K is a free K-module; i.e., it has a basis.

Русский

Векторное пространство над делением кольца K является свободным модулем над K; то есть существует базис.

LaTeX

$$$\text{Module.Free}_K V$ (i.e., there exists a basis of $V$ over $K$)$$

Lean4

@[stacks 09FN "Generalized from fields to division rings."]
instance (priority := 100) _root_.Module.Free.of_divisionRing : Module.Free K V :=
  Module.Free.of_basis (ofVectorSpace K V)

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