compLinearMap_id — Mathlib

English

Composing a multilinear map with the identity map in each argument returns the original map.

Русский

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

LaTeX

$$$ (g.compLinearMap (\\λ _ , LinearMap.id)) = g $$$

Lean4

/-- Composing a multilinear map with the identity linear map in each argument. -/
@[simp]
theorem compLinearMap_id (g : MultilinearMap R M₁' M₂) : (g.compLinearMap fun _ => LinearMap.id) = g :=
  ext fun _ => rfl

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