map_apply_ιMulti — Mathlib

English

The induced map distributes over the n-fold exterior product: map f (ιMulti R n m) = ιMulti R n (f ∘ m).

Русский

Отображение распределяется по n-разному внешнему произведению: map f (ιMulti R n m) = ιMulti R n (f ∘ m).

LaTeX

$$$ map_f(ιMulti\\_R(n)(m)) = ιMulti\\_R(n)(f \\circ m). $$$

Lean4

@[simp]
theorem map_apply_ιMulti {n : ℕ} (f : M →ₗ[R] N) (m : Fin n → M) : map f (ιMulti R n m) = ιMulti R n (f ∘ m) :=
  by
  rw [ιMulti_apply, ιMulti_apply, map_list_prod]
  simp only [List.map_ofFn, Function.comp_def, map_apply_ι]

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