zero_compLinearMap — Mathlib

English

The composition with the zero linear map yields the zero alternating map.

Русский

Композицией с нулевым линейным отображением получаем нулевое чередующее отображение.

LaTeX

$$$ (0 : N \to_{\_R} N_2).compAlternatingMap f = 0 $$$

Lean4

@[simp]
theorem zero_compLinearMap (g : M₂ →ₗ[R] M) : (0 : M [⋀^ι]→ₗ[R] N).compLinearMap g = 0 :=
  by
  ext
  simp only [compLinearMap_apply, zero_apply]

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