submodule_mk''

Mathlib.LinearAlgebra.Projectivization.Basic

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

← MathLib Explorer

English

The submodule of mk'' H h is exactly H when h asserts finrank H = 1.

Русский

Подмодуль mk'' H h равен H, когда h доказывает finrank H = 1.

LaTeX

$$$ (\mathrm mk''\ H\ h).\mathrm{submodule} = H $$$

Lean4

@[simp]
theorem submodule_mk'' (H : Submodule K V) (h : finrank K H = 1) : (mk'' H h).submodule = H :=
  congr_arg Subtype.val <| (equivSubmodule K V).apply_symm_apply ⟨H, h⟩

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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