def ContinuousAddEquiv.toIntContinuousLinearEquiv {M : Type u_1} {M₂ : Type u_2} [AddCommGroup M] [TopologicalSpace M] [AddCommGroup M₂] [TopologicalSpace M₂] (e : M ≃ₜ+ M₂) : M ≃L[ℤ] M₂

Equations

• e.toIntContinuousLinearEquiv = { toLinearEquiv := e.toIntLinearEquiv, continuous_toFun := ⋯, continuous_invFun := ⋯ }

def ContinuousAddEquiv.quotientPi {ι : Type u_1} {G : ι → Type u_2} [(i : ι) → AddCommGroup (G i)] [(i : ι) → TopologicalSpace (G i)] [∀ (i : ι), IsTopologicalAddGroup (G i)] [Fintype ι] (p : (i : ι) → AddSubgroup (G i)) [DecidableEq ι] : ((i : ι) → G i) ⧸ AddSubgroup.pi Set.univ p ≃ₜ+ ((i : ι) → G i ⧸ p i)

Equations

• ContinuousAddEquiv.quotientPi p = (Submodule.quotientPiContinuousLinearEquiv fun (i : ι) => AddSubgroup.toIntSubmodule (p i)).toContinuousAddEquiv