coe_inl — Mathlib

English

Let M and M2 be modules over a semiring R. The canonical injection of M into the product M × M2 is the map x ↦ (x, 0). In particular, (inl R M M2) = (x ↦ (x, 0)).

Русский

Пусть M и M₂ — модули над полупкольром R. Каноническое вложение M в произведение M × M₂ задаётся отображением x ↦ (x, 0). В частности, inl R M M₂ равно отображению x ↦ (x,0).

LaTeX

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

Lean4

@[simp]
theorem coe_inl : (inl R M M₂ : M → M × M₂) = fun x => (x, 0) :=
  rfl

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