mathlib3 documentation


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 #

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