alternatingMapToDual_apply_ιMulti

English

For any f: Fin n → M^*, v: Fin n → M, pairingDual applied to ιMulti(f) and ιMulti(v) equals the determinant of the matrix with entries f_j(v_i).

Русский

Для любых f: Fin n → M^*, v: Fin n → M, pairingDual применимо к ιMulti(f) и ιMulti(v) даёт детерминант матрицы со значениями f_j(v_i).

LaTeX

$$$ pairingDual\ R\ M\ n (ιMulti R\, n\, f) (ιMulti R\, n\, v) = Matrix.det (n := Fin n) (.of (fun i j \mapsto f j (v i))) $$$

Lean4

@[simp]
theorem alternatingMapToDual_apply_ιMulti {n : ℕ} (f : (_ : Fin n) → Module.Dual R M) (v : Fin n → M) :
    alternatingMapToDual R M n f (ιMulti _ _ v) = Matrix.det (n := Fin n) (.of (fun i j ↦ f j (v i))) := by
  simp [alternatingMapToDual, Matrix.det_apply]

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