pairingDual_ιMulti_ιMulti — Mathlib

English

Evaluating pairingDual on ιMulti(f) and ιMulti(v) yields the determinant of the matrix with entries f_j(v_i).

Русский

Оценивание 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 pairingDual_ιMulti_ιMulti {n : ℕ} (f : (_ : Fin n) → Module.Dual R M) (v : Fin n → M) :
    pairingDual R M n (ιMulti _ _ f) (ιMulti _ _ v) = Matrix.det (n := Fin n) (.of (fun i j ↦ f j (v i))) := by
  simp [pairingDual]

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