fst_map_fst

Mathlib.LinearAlgebra.Prod

URI: https://scilib.ai/kg/mathlib#Submodule.fst_map_fst

English

The map of fst under fst equals the identity on the top submodule.

Русский

Отображение fst под fst равно тождественному на вершине подмодуля.

LaTeX

$$$\\mathrm{fst\\, R\\, M\\, M_2}.\\mathrm{map}(\\mathrm{fst}\\, R\\, M\\, M_2) = \\top$$$

Lean4

theorem fst_map_fst : (Submodule.fst R M M₂).map (LinearMap.fst R M M₂) = ⊤ := by aesop

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

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

Разделы

Аффилиация

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