inrHom — Mathlib

English

There is a canonical R-linear inclusion map inrHom: M → tsze_R M given by the embedding inr.

Русский

Существует каноническое R-линейное вложение inrHom: M → tsze_R M, задаваемое вложением inr.

LaTeX

$$$\text{inrHom} : M \to_\mathrm{linear} tsze_{R} M \, (\text{toFun} := \mathrm{inr})$$$

Lean4

/-- The canonical `R`-linear inclusion `M → TrivSqZeroExt R M`. -/
@[simps apply]
def inrHom [Semiring R] [AddCommMonoid M] [Module R M] : M →ₗ[R] tsze R M :=
  { LinearMap.inr R R M with toFun := inr }

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