RingOfIntegers.dvd_norm

theorem RingOfIntegers.dvd_norm : ∀ {L : Type u_1} (K : Type u_2) [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L] [inst_3 : FiniteDimensional K L] [inst_4 : IsGalois K L] (x : ↥(NumberField.ringOfIntegers L)), x ∣ (algebraMap ↥(NumberField.ringOfIntegers K) ↥(NumberField.ringOfIntegers L)) ((RingOfIntegers.norm K) x)

The theorem `RingOfIntegers.dvd_norm` states that if `L/K` is a finite Galois extension of fields, then for every integer `x` in the number ring `L`, `x` divides the map from the ring of integers in `K` to the ring of integers in `L` applied to the norm of `x` from `K`. This map is defined by the algebra structure of the ring. In other words, if we consider an element `x` from the ring of integers in a number field `L` that is a finite Galois extension of another number field `K`, then `x` is a divisor of the value obtained by applying the algebra map to the norm (from `K`) of `x`.

More concisely: If `L/K` is a finite Galois extension of fields and `x` is an integer in the ring of integers of `L`, then `x` divides the norm of `x` in the algebra map from the ring of integers of `K` to the ring of integers of `L`.