trace_algebraMap_of_basis — Mathlib

English

For a basis b of S over R and s ∈ S, the trace equals the trace of the left multiplication matrix of s with respect to b.

Русский

Для базиса b базиса S над R и элемента s ∈ S след равен следу матрицы левого умножения на s в базе b.

LaTeX

$$$\\operatorname{trace}(R,S)(s) = \\operatorname{trace}( \\mathrm{leftMulMatrix}(b,s) )$$$

Lean4

/-- If `x` is in the base field `K`, then the trace is `[L : K] * x`. -/
theorem trace_algebraMap_of_basis (b : Basis ι R S) (x : R) : trace R S (algebraMap R S x) = Fintype.card ι • x :=
  by
  haveI := Classical.decEq ι
  rw [trace_apply, LinearMap.trace_eq_matrix_trace R b, Matrix.trace]
  convert Finset.sum_const x
  simp [-coe_lmul_eq_mul]

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