English
Let A be an algebra over B and b be a finite basis of A as a B-module. The matrix whose entries are the traces of products in A (the trace form) with respect to the basis b coincides with the trace matrix defined by b. In symbols, the trace matrix of A with respect to b equals the matrix of the trace form on A over B evaluated at b.
Русский
Пусть A — алгебра над B, а b — конечный базис A как B-модуля. Матрица следа, образованная по базису b и по форме следа, совпадает с матрицей следа, определяемой по базису b. То есть traceMatrix A b равна BilinForm.toMatrix b (traceForm A B).
LaTeX
$$$\\operatorname{traceMatrix}(A,b) = \\operatorname{BilinForm.toMatrix}(b,\\operatorname{traceForm}(A,B))$$$
Lean4
theorem traceMatrix_of_basis [Fintype κ] [DecidableEq κ] (b : Basis κ A B) :
traceMatrix A b = BilinForm.toMatrix b (traceForm A B) :=
by
ext (i j)
rw [traceMatrix_apply, traceForm_apply, traceForm_toMatrix]
