mk''_submodule

Mathlib.LinearAlgebra.Projectivization.Basic

URI: https://scilib.ai/kg/mathlib#Projectivization.mk''_submodule

English

For any projective point v, mk''(v.submodule, v.finrank_submodule) = v.

Русский

Для любой точки v проективного пространства верно, что mk''(v.submodule, v.finrank_submodule) = v.

LaTeX

$$$ mk''(v.submodule, v.finrank_submodule) = v $$$

Lean4

@[simp]
theorem mk''_submodule (v : ℙ K V) : mk'' v.submodule v.finrank_submodule = v :=
  (equivSubmodule K V).symm_apply_apply v

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

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

Разделы

Аффилиация

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