trace_eq_matrix_trace — Mathlib

English

If x ∈ R, the trace of its image in S is card(ι) times x, where b is a basis of S over R.

Русский

Если x ∈ R, след образа x в S равен |ι|·x, где b — базис S над R.

LaTeX

$$$\\operatorname{trace}(R,S)(\\alpha) = |\\iota| \\cdot \\alpha$ for $\\alpha \\in R$ when $b$ is a basis of $S$ over $R$$$

Lean4

theorem trace_eq_matrix_trace [DecidableEq ι] (b : Basis ι R S) (s : S) :
    trace R S s = Matrix.trace (Algebra.leftMulMatrix b s) := by
  rw [trace_apply, LinearMap.trace_eq_matrix_trace _ b, ← toMatrix_lmul_eq]; rfl

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