toPerfectPairing — Mathlib

English

An invertible matrix A over a commutative ring R defines a perfect pairing on the free module R^n with itself, yielding a nondegenerate bilinear form.

Русский

Обратимая матрица A над кольцом R задаёт совершенное парирование на свободном модуле R^n с самим собой, образуя невырожденную билинейную форму.

LaTeX

$$$A \in \mathrm{GL}_n(R) \quad\Longrightarrow\quad \text{A induces a PerfectPairing } R^{n} \times R^{n} \to R$$$

Lean4

/-- We may regard an invertible matrix as a perfect pairing. -/
@[deprecated "No replacement" (since := "2025-08-16")]
def toPerfectPairing : PerfectPairing R (n → R) (n → R) :=
  ((A.toLinearEquiv' h).trans (dotProductEquiv R n)).toPerfectPairing

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