fst_map_snd

Mathlib.LinearAlgebra.Prod

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

English

The image of the fst-submodule under snd is the bottom submodule.

Русский

Образ fst-подмодуля под snd равен нижнему подмодулю.

LaTeX

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

Lean4

theorem fst_map_snd : (Submodule.fst R M M₂).map (LinearMap.snd R M M₂) = ⊥ := by aesop (add simp fst)

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

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

Разделы

Аффилиация

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