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 #

Main results #

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

Instances For
    theorem RingOfIntegers.coe_norm {L : Type u_1} (K : Type u_2) [Field K] [Field L] [Algebra K L] [FiniteDimensional K L] [IsSeparable K L] (x : NumberField.RingOfIntegers L) :
    ((RingOfIntegers.norm K) x) = (Algebra.norm K) 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).