traceMatrix_reindex — Mathlib

English

The (i,j) entry of the trace matrix equals the trace of (b_i, b_j) under the trace form.

Русский

(i,j)-й элемент матрицы следа равен произведению следа формы на элементе b_i, b_j.

LaTeX

$$$\\operatorname{traceMatrix}_{A}(b)_{ij} = \\mathrm{traceForm}_{A,B}(b_i,b_j)$$$

Lean4

theorem traceMatrix_reindex {κ' : Type*} (b : Basis κ A B) (f : κ ≃ κ') :
    traceMatrix A (b.reindex f) = reindex f f (traceMatrix A b) := by ext (x y); simp

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