theorem Submodule.Quotient.indiscreteTopology_iff {R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] [TopologicalSpace M] [IsTopologicalAddGroup M] [ContinuousConstSMul R M] {S : Submodule R M} : IndiscreteTopology (M ⧸ S) ↔ S.topologicalClosure = ⊤

theorem Submodule.Quotient.indiscreteTopology {R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] [TopologicalSpace M] [IsTopologicalAddGroup M] [ContinuousConstSMul R M] {S : Submodule R M} : S.topologicalClosure = ⊤ → IndiscreteTopology (M ⧸ S)

Alias of the reverse direction of Submodule.Quotient.indiscreteTopology_iff.

theorem Submodule.Quotient.topologicalClosure_eq_top {R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] [TopologicalSpace M] [IsTopologicalAddGroup M] [ContinuousConstSMul R M] (S : Submodule R M) [IndiscreteTopology (M ⧸ S)] : S.topologicalClosure = ⊤

theorem Submodule.Quotient.nontrivialTopology_iff {R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] [TopologicalSpace M] [IsTopologicalAddGroup M] [ContinuousConstSMul R M] {S : Submodule R M} : NontrivialTopology (M ⧸ S) ↔ S.topologicalClosure ≠ ⊤

theorem Submodule.Quotient.nontrivialTopology {R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] [TopologicalSpace M] [IsTopologicalAddGroup M] [ContinuousConstSMul R M] {S : Submodule R M} : S.topologicalClosure ≠ ⊤ → NontrivialTopology (M ⧸ S)

Alias of the reverse direction of Submodule.Quotient.nontrivialTopology_iff.

theorem Submodule.Quotient.topologicalClosure_ne_top {R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] [TopologicalSpace M] [IsTopologicalAddGroup M] [ContinuousConstSMul R M] (S : Submodule R M) [NontrivialTopology (M ⧸ S)] : S.topologicalClosure ≠ ⊤