comap_snd

Mathlib.LinearAlgebra.Prod

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

English

Let f: M → M₃ and g: M₂ → M₃. Then (ker f) × (ker g) ⊆ ker(f.coprod g).

Русский

Пусть f: M → M₃ и g: M₂ → M₃. Тогда (ker f) × (ker g) ⊆ ker(f.coprod g).

LaTeX

$$$(\\ker f) \\times (\\ker g) \\subseteq \\ker(f \\ coprod\\ g).$$$

Lean4

@[simp]
theorem comap_snd : q.comap (snd R M M₂) = prod ⊤ q := by ext ⟨x, y⟩; simp

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

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

Разделы

Аффилиация

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