English
The trace of an algebra element with respect to a basis equals the sum of its action in the corresponding diagonal form.
Русский
След элемента алгебры по базису равен сумме действий в диагональной форме.
LaTeX
$$$\\text{trace\_trace\_of\_basis} = \\sum_i L_{b_i}$$$
Lean4
theorem trace_trace_of_basis [Algebra S T] [IsScalarTower R S T] {ι κ : Type*} [Finite ι] [Finite κ] (b : Basis ι R S)
(c : Basis κ S T) (x : T) : trace R S (trace S T x) = trace R T x :=
by
haveI := Classical.decEq ι
haveI := Classical.decEq κ
cases nonempty_fintype ι
cases nonempty_fintype κ
rw [trace_eq_matrix_trace (b.smulTower c), trace_eq_matrix_trace b, trace_eq_matrix_trace c, Matrix.trace,
Matrix.trace, Matrix.trace, ← Finset.univ_product_univ, Finset.sum_product]
refine Finset.sum_congr rfl fun i _ ↦ ?_
simp only [map_sum, smulTower_leftMulMatrix, Finset.sum_apply, Matrix.diag,
Finset.sum_apply i (Finset.univ : Finset κ) fun y => leftMulMatrix b (leftMulMatrix c x y y)]
