∀ {A : Type u_8} {B : Type u_9} {C : Type u_10} [inst : CommRing A] [inst_1 : CommRing B] [inst_2 : Ring C]
  [inst_3 : Algebra A C] [inst_4 : Algebra B C] (e : A ≃+* B),
  (algebraMap B C).comp ↑e = algebraMap A C → ∀ (x : C), e ((Algebra.norm A) x) = (Algebra.norm B) x