Documentation

Mathlib.NumberTheory.NumberField.Norm

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 between the rings of integers.

Equations
Instances For
    @[simp]

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