instFiniteDimensionalSubtypeMemSubmoduleSubmodule

English

For any projective point v, the associated subspace v.submodule is finite-dimensional over K.

Русский

Для любой точки проекта размерность подпространства v.submodule по отношению к K конечна.

LaTeX

$$$\operatorname{FiniteDimensional}_K(v.\mathrm{submodule})$$$

Lean4

instance (v : ℙ K V) : FiniteDimensional K v.submodule :=
  by
  rw [← v.mk_rep]
  change FiniteDimensional K (K ∙ v.rep)
  infer_instance

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