submodule_eq

Mathlib.LinearAlgebra.Projectivization.Basic

URI: https://scilib.ai/kg/mathlib#Projectivization.submodule_eq

English

For any v ∈ ℙ_K(V), the associated submodule equals the Span of its representative, i.e. v.submodule = span_K{ v.rep }.

Русский

Для любого v ∈ ℙ_K(V) соответствующее подпространство равно span_K{ v.rep }.

LaTeX

$$$ v.\mathrm{submodule} = \operatorname{span}_K\{ v.rep \} $$$

Lean4

theorem submodule_eq (v : ℙ K V) : v.submodule = K ∙ v.rep :=
  by
  conv_lhs => rw [← v.mk_rep]
  rfl

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru