finrank_submodule — Mathlib

English

For any v ∈ ℙ_K(V), the subspace v.submodule has finite dimension over K and is of dimension 1.

Русский

Для любого v ∈ ℙ_K(V) подпространство v.submodule конечномерно над K и имеет размерность 1.

LaTeX

$$$\operatorname{finrank}_K(v.\mathrm{submodule}) = 1$$$

Lean4

theorem finrank_submodule (v : ℙ K V) : finrank K v.submodule = 1 :=
  by
  rw [submodule_eq]
  exact finrank_span_singleton v.rep_nonzero

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