traceForm_toMatrix_powerBasis — Mathlib

English

If h is a power basis of S over R, the matrix of the trace bilinear form, written in the basis given by h, has (i,j)-entry equal to Tr_R,S(h.gen^(i+j)).

Русский

Если h — степенной базис S над R, матрица формы следа, записанная в базисе h, имеет (i,j)-й элемент равный Tr_R,S(h.gen^(i+j)).

LaTeX

$$$\\mathrm{BilinForm.toMatrix}\\,h.basis\\, (\\mathrm{traceForm}\\, R\\, S) = \\mathrm{Of}\\bigl( i,j \\mapsto \\mathrm{trace}_{R,S}(h.gen^{\\,i+j}) \\bigr)$$$

Lean4

theorem traceForm_toMatrix_powerBasis (h : PowerBasis R S) :
    BilinForm.toMatrix h.basis (traceForm R S) = of fun i j => trace R S (h.gen ^ (i.1 + j.1)) := by ext;
  rw [traceForm_toMatrix, of_apply, pow_add, h.basis_eq_pow, h.basis_eq_pow]

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