sndHom — Mathlib

English

There is a canonical R-linear projection sndHom: tsze_R M → M with toFun := snd.

Русский

Существует каноническое линейное проецирование sndHom: tsze_R M → M, где toFun = snd.

LaTeX

$$$\text{sndHom} : tsze_{R} M \to_{\mathrm{linear}} M \; (\text{toFun} := \mathrm snd)$$$

Lean4

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

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