compLinearMap_id — Mathlib

English

Let f be an alternating R-linear map with ι arguments from M to N. Composing f with the identity linear map on M in each argument leaves f unchanged.

Русский

Пусть f — чередующая R-линейная карта с ι аргументов, от M к N. Композиция f с единичным линейным отображением по каждому аргументу не изменяет f.

LaTeX

$$$ f \\circ_{\mathrm{lin}} \\mathrm{id} = f $$$

Lean4

/-- Composing an alternating map with the identity linear map in each argument. -/
@[simp]
theorem compLinearMap_id (f : M [⋀^ι]→ₗ[R] N) : f.compLinearMap LinearMap.id = f :=
  ext fun _ => rfl

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