English
Let b be a basis of A over B. For z in B, the product of the trace matrix with the coordinate vector of z in the basis b gives the vector of traces Tr_A,B(z b_i) for each basis vector b_i.
Русский
Пусть b — базис A над B. Для z ∈ B произведение traceMatrix(A,b) на координатный столбец z в базисе b дает вектор значений Tr_A,B(z b_i) по всем базисным векторам b_i.
LaTeX
$$$\\operatorname{traceMatrix}(A,b) \\cdot\\!^{\\vee} (b\\,\\mathrm{equivFun}\\; z) = \\big( \\operatorname{trace}(A,B)(z \\cdot b_i) \\big)_{i}$$$
Lean4
theorem traceMatrix_of_basis_mulVec (b : Basis ι A B) (z : B) :
traceMatrix A b *ᵥ b.equivFun z = fun i => trace A B (z * b i) :=
by
ext i
rw [← replicateCol_apply (ι := Fin 1) (traceMatrix A b *ᵥ b.equivFun z) i 0, replicateCol_mulVec, Matrix.mul_apply,
traceMatrix]
simp only [replicateCol_apply, traceForm_apply]
conv_lhs =>
congr
rfl
ext
rw [mul_comm _ (b.equivFun z _), ← smul_eq_mul, of_apply, ← LinearMap.map_smul]
rw [← _root_.map_sum]
congr
conv_lhs =>
congr
rfl
ext
rw [← mul_smul_comm]
rw [← Finset.mul_sum, mul_comm z]
congr
rw [b.sum_equivFun]
