normalizedTrace_surjective — Mathlib

English

The normalized trace map Tr_{F}^{K}: K → F is surjective; every element of F is realized as a trace of some element of K.

Русский

Нормализованный след отображает K на F сюръективно; каждый элемент F является следом некоторого элемента K.

LaTeX

$$There exists x ∈ K such that normalizedTrace F K (x) = b for every b ∈ F.$$

Lean4

theorem normalizedTrace_surjective : Function.Surjective (normalizedTrace F K) := fun a ↦
  ⟨algebraMap F K a, normalizedTrace_algebraMap_apply_eq_self F K a⟩

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