map_comp_ιMulti — Mathlib

English

For any v: Fin (n+1) → M, ιMulti R (n+1) v = ι_R(v(0)) · ιMulti R n (Matrix.vecTail v).

Русский

Для любой v: Fin (n+1) → M, ιMulti R (n+1) v = ι_R(v(0)) · ιMulti R n (Matrix.vecTail v).

LaTeX

$$$ ιMulti\\_R(n+1)(v) = ι_R(v(0)) \\cdot ιMulti\\_R(n)(Matrix.vecTail(v)). $$$

Lean4

@[simp]
theorem map_comp_ιMulti {n : ℕ} (f : M →ₗ[R] N) :
    (map f).toLinearMap.compAlternatingMap (ιMulti R n (M := M)) = (ιMulti R n (M := N)).compLinearMap f :=
  by
  ext m
  exact map_apply_ιMulti _ _

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