prod_comap_inl

Mathlib.LinearAlgebra.Prod

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

English

If range f and range g are disjoint, ker(f.coprod g) equals (ker f) × (ker g).

Русский

Если образы range f и range g не пересекаются, то ker(f.coprod g) = (ker f) × (ker g).

LaTeX

$$$\\ker(f \\ coprod\\ g) = (\\ker f) \\ times (\\ker g)\\quad\\text{if }\\; \\mathrm{range}(f) \\cap \\mathrm{range}(g) = \\{0\\}.$$$

Lean4

@[simp]
theorem prod_comap_inl : (prod p q).comap (inl R M M₂) = p := by ext; simp

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

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

Разделы

Аффилиация

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