normalizedTrace_intermediateField

English

Restriction of normalized trace to an intermediate field E ⊆ K equals the normalized trace from F to E.

Русский

Ограничение нормализованного следа к промежуточному полю E совпадает с нормализованным следом из F в E.

LaTeX

$$$\text{normalizedTrace } F K|_E = \text{normalizedTrace } F E$$$

Lean4

/-- The normalized trace transfers via restriction to a subextension. -/
theorem normalizedTrace_intermediateField {E : IntermediateField F K} (a : E) :
    normalizedTrace F K a = normalizedTrace F E a :=
  normalizedTraceAux_intermediateField F K a

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