normalizedTrace_trans — Mathlib

English

For towers F ⊆ E ⊆ K with appropriate integrality, the composition of normalized trace maps equals the direct trace: Tr_F^E ∘ Tr_E^K = Tr_F^K.

Русский

Для цепи F ⊆ E ⊆ K выполняется композиция нормализованных следов: Tr_F^E ∘ Tr_E^K = Tr_F^K.

LaTeX

$$$\\operatorname{normalizedTrace}_{F}^{E} \circ \operatorname{normalizedTrace}_{E}^{K} = \\operatorname{normalizedTrace}_{F}^{K}$$$

Lean4

@[simp]
theorem normalizedTrace_trans [Algebra.IsIntegral E K] [CharZero E] :
    normalizedTrace F E ∘ₗ normalizedTrace E K = normalizedTrace F K :=
  LinearMap.ext <| normalizedTrace_trans_apply F E K

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