def Submodule.Quotient.continuousLinearEquiv {R : Type u_1} [Ring R] (G : Type u_2) (H : Type u_3) [AddCommGroup G] [Module R G] [AddCommGroup H] [Module R H] [TopologicalSpace G] [TopologicalSpace H] (G' : Submodule R G) (H' : Submodule R H) (e : G ≃L[R] H) (h : map (↑e.toLinearEquiv) G' = H') : (G ⧸ G') ≃L[R] H ⧸ H'

def Submodule.quotientPiContinuousLinearEquiv {R : Type u_1} {ι : Type u_2} [CommRing R] {G : ι → Type u_3} [(i : ι) → AddCommGroup (G i)] [(i : ι) → Module R (G i)] [(i : ι) → TopologicalSpace (G i)] [∀ (i : ι), IsTopologicalAddGroup (G i)] [Fintype ι] [DecidableEq ι] (p : (i : ι) → Submodule R (G i)) : (((i : ι) → G i) ⧸ pi Set.univ p) ≃L[R] (i : ι) → G i ⧸ p i