toPerfectPairing_apply_apply — Mathlib

English

For an invertible matrix A and vectors v, w, the evaluation of the induced perfect pairing equals the standard matrix-dotted product A v · w.

Русский

Для обратимой матрицы A и векторов v, w вычисление полученного совершенного парирования даёт обычное произведение матрицы A на v скалярно на w.

LaTeX

$$$A.toPerfectPairing\; h\; v\; w = (A \cdot v) \cdot w$$$

Lean4

@[deprecated "No replacement" (since := "2025-08-16")]
theorem toPerfectPairing_apply_apply (v w : n → R) : A.toPerfectPairing h v w = A *ᵥ v ⬝ᵥ w :=
  rfl

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