Quotients of a topological module by an open submodule

The quotient of a topological module by an open submodule is discrete; in particular the quotient of a discrete topological module by any submodule is discrete, since in a discrete module every submodule is open.

Mathlib's QuotientAddGroup.discreteTopology is the statement for the quotient of a topological additive group by an open subgroup, and supplies the whole proof; because it is a theorem rather than an instance (Mathlib notes that IsOpen would have to be a class for that), instance search cannot use it, so this file records it for M ⧸ p as a theorem, and the discrete case as an instance. This is the same bridge from QuotientAddGroup to Submodule.Quotient that Mathlib's own Submodule.isTopologicalAddGroup_quotient and Submodule.t3_quotient_of_isClosed provide.

theorem Submodule.Quotient.discreteTopology_of_isOpen {R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] [TopologicalSpace M] [SeparatelyContinuousAdd M] (p : Submodule R M) (hp : IsOpen ↑p) : DiscreteTopology (M ⧸ p)

The quotient of a topological module by an open submodule is discrete.

instance Submodule.Quotient.discreteTopology {R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] [TopologicalSpace M] [SeparatelyContinuousAdd M] [DiscreteTopology M] (p : Submodule R M) : DiscreteTopology (M ⧸ p)

The quotient of a discrete topological module by a submodule is discrete.