prod_map_fst

Mathlib.LinearAlgebra.Prod

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

English

For submodules p ⊆ M and q ⊆ M₂, (prod p q).comap (inl R M M₂) = p.

Русский

Для p ⊆ M и q ⊆ M₂ верно (prod p q).comap (inl R M M₂) = p.

LaTeX

$$$ (\\mathrm{prod}\, p\\, q).\\mathrm{comap}(\\mathrm{inl}\\, R\\, M\\, M_2) = p $$$

Lean4

@[simp]
theorem prod_map_fst : (prod p q).map (fst R M M₂) = p := by ext x; simp [(⟨0, zero_mem _⟩ : ∃ x, x ∈ q)]

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

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

Разделы

Аффилиация

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