∀ (𝕜 : Type u_2) (𝕜' : Type u_3) (E : Type u_1) [inst : NormedField 𝕜] [inst_1 : NormedField 𝕜']
  [inst_2 : NormedAlgebra 𝕜 𝕜'] [inst_3 : SeminormedRing E] [inst_4 : NormedAlgebra 𝕜' E] (r : 𝕜) (x : E),
  Algebra.algebraMap r * x = x * Algebra.algebraMap r