Subspace — Mathlib

English

A subspace of a vector space is simply a submodule over the base field (division ring).

Русский

Подпространство векторного пространства есть просто подмодуль над полем (разделяющей кольцом).

LaTeX

$$Subspace(R,M) = Submodule(R,M)$$

Lean4

/-- Subspace of a vector space. Defined to equal `Submodule`. -/
abbrev Subspace (R : Type u) (M : Type v) [DivisionRing R] [AddCommGroup M] [Module R M] :=
  Submodule R M

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