id_compMultilinearMap — Mathlib

English

Composing with the identity linear map on the codomain leaves the multilinear map unchanged: (id_M2).compMultilinearMap f = f.

Русский

Композиция с единичным линейным отображением на кодомаппинг сохраняет мультиленейное отображение: (id).compMultilinearMap f = f.

LaTeX

$$$$(\mathrm{id}: M_2 \to M_2)\;\mathrm{compMultilinearMap}\; f = f,$$ i.e. $(\mathrm{id}_{M_2}\circ f)=f$.$$

Lean4

@[simp]
theorem id_compMultilinearMap (f : MultilinearMap R M₁ M₂) : (id : M₂ →ₗ[R] M₂).compMultilinearMap f = f :=
  rfl

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