ker_inl

Mathlib.LinearAlgebra.Prod

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

English

ker(inl) = 0, i.e. the embedding is injective.

Русский

ядро inl = 0, то есть встроение инъективно.

LaTeX

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

Lean4

@[simp]
theorem ker_inl : ker (inl R M M₂) = ⊥ := by rw [ker, ← prod_bot, prod_comap_inl]

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

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

Разделы

Аффилиация

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