α✝ : Type ?u.323008
α : Type u
r : CommRing α
inst✝² : UniformSpace α
inst✝¹ : UniformAddGroup α
inst✝ : TopologicalRing α
⊢ Quotient (Submodule.quotientRel (Ideal.closure ⊥)) = (α ⧸ Ideal.closure ⊥)
α✝ : Type ?u.323008
α : Type u
r : CommRing α
inst✝² : UniformSpace α
inst✝¹ : UniformAddGroup α
inst✝ : TopologicalRing α
⊢ Quotient (separationSetoid α) = (α ⧸ Ideal.closure ⊥)
rw [@ring_sep_rel α r]
no goals
α✝ : Type ?u.323008
α : Type u
r : CommRing α
inst✝² : UniformSpace α
inst✝¹ : UniformAddGroup α
inst✝ : TopologicalRing α
⊢ Quotient (Submodule.quotientRel (Ideal.closure ⊥)) = (α ⧸ Ideal.closure ⊥)
rfl