∀ {L : Type u_1} (K : Type u_2) [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L]
  (x : NumberField.RingOfIntegers K),
  (algebraMap (NumberField.RingOfIntegers K) K)
      ((RingOfIntegers.norm K) ((algebraMap (NumberField.RingOfIntegers K) (NumberField.RingOfIntegers L)) x)) =
    (Algebra.norm K) ((algebraMap K L) ((algebraMap (NumberField.RingOfIntegers K) K) x))