inl_apply

Mathlib.LinearAlgebra.Prod

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

English

For every x in M, applying the left injection yields the pair (x, 0) in M × M₂.

Русский

для каждого x в M применение левого вложения даёт пару (x, 0) в M × M₂.

LaTeX

$$$ (inl\\, R\\, M\\, M_2)\\, x = (x,0) $$$

Lean4

theorem inl_apply (x : M) : inl R M M₂ x = (x, 0) :=
  rfl

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

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

Разделы

Аффилиация

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