mathlib documentation


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 #

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