trace — Mathlib

English

After base change to E, the trace matrix equals the product of the embeddings matrix with its transpose.

Русский

После переключения базы в E матрица следа равна произведению матрицы вложений на её транспонированную.

LaTeX

$$$\\big(\\mathrm{traceMatrix}(K,b)\\big)^{\\mapsto (algebraMap\\;K\\;E)} = \\mathrm{embeddingsMatrix}(K,E,b) \\cdot \\big(\\mathrm{embeddingsMatrix}(K,E,b)\\big)^{\\top}$$$

Lean4

/-- The trace of an element `s` of an `R`-algebra is the trace of `(s * ·)`,
as an `R`-linear map. -/
@[stacks 0BIF "Trace"]
noncomputable def trace : S →ₗ[R] R :=
  (LinearMap.trace R S).comp (lmul R S).toLinearMap

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