# mathlib3documentation

number_theory.number_field.norm

# Norm in number fields #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4. Given a finite extension of number fields, we define the norm morphism as a function between the rings of integers.

## Main definitions #

• ring_of_integers.norm K : algebra.norm as a morphism (π L) β* (π K).

## Main results #

• algebra.dvd_norm : 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).
@[simp]
theorem ring_of_integers.norm_apply_coe {L : Type u_1} (K : Type u_2) [field K] [field L] [ L] [ L] [ L] (n : β₯) :
noncomputable def ring_of_integers.norm {L : Type u_1} (K : Type u_2) [field K] [field L] [ L] [ L] [ L] :

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

Equations
theorem ring_of_integers.coe_algebra_map_norm {L : Type u_1} (K : Type u_2) [field K] [field L] [ L] [ L] [ L] (x : β₯) :
theorem ring_of_integers.coe_norm_algebra_map {L : Type u_1} (K : Type u_2) [field K] [field L] [ L] [ L] [ L] (x : β₯) :
theorem ring_of_integers.norm_algebra_map {L : Type u_1} (K : Type u_2) [field K] [field L] [ L] [ L] [ L] (x : β₯) :
theorem ring_of_integers.is_unit_norm_of_is_galois {L : Type u_1} (K : Type u_2) [field K] [field L] [ L] [ L] [ L] {x : β₯} :
theorem ring_of_integers.dvd_norm {L : Type u_1} (K : Type u_2) [field K] [field L] [ L] [ L] [ L] (x : β₯) :

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).

theorem ring_of_integers.norm_norm {L : Type u_1} (K : Type u_2) [field K] [field L] [ L] [ L] (F : Type u_3) [field F] [ F] [ F] [ F] [ L] [ L] [ L] [ L] [ L] (x : β₯) :
x) =
theorem ring_of_integers.is_unit_norm (K : Type u_2) [field K] {F : Type u_3} [field F] [ F] [ F] [ F] [char_zero K] {x : β₯} :