zero_compLinearMap — Mathlib

English

Composing the zero multilinear map with any family of linear maps yields the zero multilinear map.

Русский

Композиция нулевой мультиленейной карты с любыми линейными отображениями даёт нулевую мультиленейную карту.

LaTeX

$$$ (0 : MultilinearMap R M_1' M_2).compLinearMap f = 0 $$$

Lean4

/-- Composing the zero multilinear map with a linear map in each argument. -/
@[simp]
theorem zero_compLinearMap (f : ∀ i, M₁ i →ₗ[R] M₁' i) : (0 : MultilinearMap R M₁' M₂).compLinearMap f = 0 :=
  ext fun _ => rfl

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