ker_fst

Mathlib.LinearAlgebra.Prod

URI: https://scilib.ai/kg/mathlib#LinearMap.ker_fst

English

The range of the left injection inl R M M2 equals the kernel of the second projection snd R M M2.

Русский

Образ левой инъекции inl равенker второму проекции snd.

LaTeX

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

Lean4

theorem ker_fst : ker (fst R M M₂) = range (inr R M M₂) :=
  Eq.symm <| range_inr R M M₂

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

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

Разделы

Аффилиация

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