normalizedTrace_map — Mathlib

English

The normalized trace commutes with an injective algebra morphism f: E→K: normalizing after applying f equals applying f after normalizing on E.

Русский

Согласование нормализованного следа с инъективным алгебровым отображением: последовательное применение f и нормализованный след совпадают.

LaTeX

$$$\text{normalizedTrace } F K \circ f = f \circ \text{normalizedTrace } F E$$$

Lean4

/-- The normalized trace transfers via (injective) maps. -/
@[simp]
theorem normalizedTrace_map {E : Type*} [Field E] [Algebra F E] [Algebra.IsIntegral F E] (f : E →ₐ[F] K) (a : E) :
    normalizedTrace F K (f a) = normalizedTrace F E a :=
  normalizedTraceAux_map F K f a

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