English
For finite extensions L/K and x ∈ L, the K-norm of x is expressed via the minpoly of x over K and its roots in an extension F, yielding a product formula.
Русский
Для конечного расширения L/K и элемента x∈L норма K(x) выражается через минимальный многочлен x над K и его корни в некоем расширении F.
LaTeX
$$$\\mathrm{norm}_K(x) = (\\mathrm{minpoly}_K x)\\text{-root-product}^{\\mathrm{finrank}_K(⟮x⟯L)}$$$
Lean4
theorem norm_eq_norm_adjoin (x : L) : norm K x = norm K (AdjoinSimple.gen K x) ^ finrank K⟮x⟯ L :=
by
by_cases h : FiniteDimensional K L
swap
· rw [norm_eq_one_of_not_module_finite h]
by_cases hx : IsIntegral K x
· have h₁ : ¬FiniteDimensional K⟮x⟯ L := fun H ↦
h <| by
have : FiniteDimensional K K⟮x⟯ := adjoin.finiteDimensional hx
exact Finite.trans K⟮x⟯ L
simp [finrank_of_not_finite h₁]
· rw [norm_eq_one_of_not_module_finite]
· simp
· refine fun H ↦ hx ?_
rw [← isIntegral_gen]
exact IsIntegral.isIntegral (gen K x)
let F := K⟮x⟯
nth_rw 1 [← coe_gen K x]
rw [← norm_norm (S := F), ← IntermediateField.algebraMap_apply,
norm_algebraMap_of_basis (Module.Free.chooseBasis F L) (gen K x), map_pow, finrank_eq_card_chooseBasisIndex]
