norm_surjective — Mathlib

English

The field norm map from K' to K is surjective for finite field extensions.

Русский

Отображение нормы из поля-расширения на базовое поле сюръективно.

LaTeX

$$Algebra.norm K : K' → K is surjective$$

Lean4

theorem norm_surjective : Function.Surjective (Algebra.norm K (S := K')) := fun k ↦
  by
  obtain rfl | ne := eq_or_ne k 0
  · exact ⟨0, Algebra.norm_zero ..⟩
  have ⟨x, eq⟩ := unitsMap_norm_surjective K K' (Units.mk0 k ne)
  exact ⟨x, congr_arg (·.1) eq⟩

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