ιMulti_succ_apply — Mathlib

English

For v: Fin (n+1) → M, the (n+1)-fold exterior product equals the first factor ι_R(v(0)) times the n-fold exterior product of the tail: ι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)(\\text{vecTail}(v)). $$$

Lean4

@[simp]
theorem ιMulti_succ_apply {n : ℕ} (v : Fin n.succ → M) : ιMulti R _ v = ι R (v 0) * ιMulti R _ (Matrix.vecTail v) := by
  simp [ιMulti, Matrix.vecTail]

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