∀ {R : Type u_1} [inst : SeminormedCommRing R] (I : Ideal R) (𝕜 : Type u_2) [inst_1 : NormedField 𝕜]
  [inst_2 : NormedAlgebra 𝕜 R] (r : 𝕜) (x : R ⧸ I), Algebra.algebraMap r * x = x * Algebra.algebraMap r