# Norm in number fields #

Given a finite extension of number fields, we define the norm morphism as a function between the rings of integers.

## Main definitions #

• RingOfIntegers.norm K : Algebra.norm as a morphism (𝓞 L) →* (𝓞 K).

## Main results #

• RingOfIntegers.dvd_norm : if L/K is a finite Galois extension of fields, then, for all (x : 𝓞 L) we have that x ∣ algebraMap (𝓞 K) (𝓞 L) (norm K x).
theorem Algebra.coe_norm_int {K : Type u_1} [] [] (x : ) :
( x) = x
theorem Algebra.coe_trace_int {K : Type u_1} [] [] (x : ) :
() = () x
noncomputable def RingOfIntegers.norm {L : Type u_1} (K : Type u_2) [] [] [Algebra K L] [] [] :

Algebra.norm as a morphism betwen the rings of integers.

Equations
Instances For
@[simp]
theorem RingOfIntegers.coe_norm {L : Type u_1} (K : Type u_2) [] [] [Algebra K L] [] [] (x : ) :
( x) = () x
theorem RingOfIntegers.coe_algebraMap_norm {L : Type u_1} (K : Type u_2) [] [] [Algebra K L] [] [] (x : ) :
() = () (() x)
theorem RingOfIntegers.algebraMap_norm_algebraMap {L : Type u_1} (K : Type u_2) [] [] [Algebra K L] [] [] (x : ) :
() () = () (() (() x))
theorem RingOfIntegers.norm_algebraMap {L : Type u_1} (K : Type u_2) [] [] [Algebra K L] [] [] (x : ) :
=
theorem RingOfIntegers.isUnit_norm_of_isGalois {L : Type u_1} (K : Type u_2) [] [] [Algebra K L] [] [IsGalois K L] {x : } :
IsUnit ( x)
theorem RingOfIntegers.dvd_norm {L : Type u_1} (K : Type u_2) [] [] [Algebra K L] [] [IsGalois K L] (x : ) :
x

If L/K is a finite Galois extension of fields, then, for all (x : 𝓞 L) we have that x ∣ algebraMap (𝓞 K) (𝓞 L) (norm K x).

theorem RingOfIntegers.norm_norm {L : Type u_1} (K : Type u_2) [] [] [Algebra K L] [] (F : Type u_3) [] [Algebra K F] [] [] [] [Algebra F L] [] [] [] (x : ) :
( x) = x
theorem RingOfIntegers.isUnit_norm (K : Type u_2) [] {F : Type u_3} [] [Algebra K F] [] [] [] {x : } :
IsUnit ( x)