English
For finite field extensions, the norm map on units is surjective.
Русский
Для конечных полей отображение нормы на единицах сюрьективно.
LaTeX
$$Units.map (Algebra.norm K) : (K' )^{\times} → (K)^{\times} is surjective$$
Lean4
theorem unitsMap_norm_surjective : Function.Surjective (Units.map <| Algebra.norm K (S := K')) :=
have := Finite.of_injective_finite_range (algebraMap K K').injective
MonoidHom.surjective_of_card_ker_le_div _ <| by
simp_rw [Nat.card_units]
classical
have := Fintype.ofFinite K'ˣ
convert
IsCyclic.card_pow_eq_one_le (α := K'ˣ) <|
Nat.div_pos (Nat.sub_le_sub_right (Nat.card_le_card_of_injective _ (algebraMap K K').injective) _) <|
Nat.sub_pos_of_lt Finite.one_lt_card
rw [← Set.ncard_coe_finset, ← SetLike.coe_sort_coe, Nat.card_coe_set_eq]; congr; ext
simp [Units.ext_iff, ← (algebraMap K K').injective.eq_iff, algebraMap_norm_eq_pow]
