∀ {A : Type u_1} (B : Type u_2) [inst : CommRing A] [inst_1 : CommRing B] [inst_2 : Algebra A B] (I : Ideal A),
  AddEquivClass ((B ⧸ Ideal.map (algebraMap A B) I) ≃ₗ[A] TensorProduct A B (A ⧸ I)) (B ⧸ Ideal.map (algebraMap A B) I)
    (TensorProduct A B (A ⧸ I))