trace_smulRight — Mathlib

English

Let f: M → R be linear and x ∈ M. The trace of the rank-one operator m ↦ f(m)·x equals f(x).

Русский

Пусть f: M → R линейно и x ∈ M. След рангового оператора m ↦ f(m)·x равен f(x).

LaTeX

$$$ \operatorname{trace}_R M (f .\!\mathrm{smulRight} x) = f(x). $$$

Lean4

@[simp]
theorem trace_smulRight (f : M →ₗ[R] R) (x : M) : trace R M (f.smulRight x) = f x :=
  by
  rw [trace_eq_matrix_trace _ (Free.chooseBasis R M), ← (Free.chooseBasis R M).sum_repr x]
  simp [-Basis.sum_repr, dotProduct]

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