inl_eq_prod — Mathlib

English

The left injection equals the product of the identity on M and the zero map on M₂, i.e., inl R M M₂ = id × 0.

Русский

Левое вложение равно произведению тождественного отображения на M и нулевого отображения на M₂, т.е. inl R M M₂ = id × 0.

LaTeX

$$$ inl\\, R\\, M\\, M_2 = \\mathrm{id}_M \\times 0 $$$

Lean4

theorem inl_eq_prod : inl R M M₂ = prod LinearMap.id 0 :=
  rfl

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