map_inr

Mathlib.LinearAlgebra.Prod

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

English

The kernel of the injection inl is trivial: ker(inl) = 0.

Русский

Ядро внедрения inl тривиально: ker(inl) = 0.

LaTeX

$$$\\ker(\\mathrm{inl}\\, R\\, M\\, M_2) = \\bot$$$

Lean4

@[simp]
theorem map_inr : q.map (inr R M M₂) = prod ⊥ q := by ext ⟨x, y⟩; simp [and_left_comm, eq_comm, and_comm]

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

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

Разделы

Аффилиация

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