normalizedTrace_algebraMap_eq_id — Mathlib

English

The normalized trace is a left inverse of the algebra map from F to K: Tr_{F}^{K} ∘ algebraMap_{F}^{K} = id on F.

Русский

Нормализованный след является левой обратной алгебраическому отображению F → K: Tr_{F}^{K} ∘ algebraMap_{F}^{K} = id на F.

LaTeX

$$$\\operatorname{normalizedTrace}_{F}^{K} \circ\\\\mathrm{Algebra.linearMap}_{F}^{K} = \\mathrm{LinearMap.id}_{F}$$$

Lean4

/-- The normalized trace map is a left inverse of the algebra map. -/
theorem normalizedTrace_algebraMap_eq_id : normalizedTrace F K ∘ₗ Algebra.linearMap F K = LinearMap.id :=
  LinearMap.ext <| normalizedTrace_algebraMap_apply_eq_self F K

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