From 330b78e284acaa7f35e8ac864f14ee1e54d9490e Mon Sep 17 00:00:00 2001
From: Alex J Best <alex.j.best@gmail.com>
Date: Wed, 23 Aug 2023 08:58:07 +0000
Subject: [PATCH] feat: add a coe to ideal quotient rings (#6620)

Like we have for (Add)Subgroups already
---
 Mathlib/GroupTheory/Coset.lean         | 2 +-
 Mathlib/RingTheory/Ideal/Quotient.lean | 3 +++
 2 files changed, 4 insertions(+), 1 deletion(-)

diff --git a/Mathlib/GroupTheory/Coset.lean b/Mathlib/GroupTheory/Coset.lean
index 11a32583789f3..6f0dc57e1d8d5 100644
--- a/Mathlib/GroupTheory/Coset.lean
+++ b/Mathlib/GroupTheory/Coset.lean
@@ -481,7 +481,7 @@ theorem induction_on {C : α ⧸ s → Prop} (x : α ⧸ s) (H : ∀ z, C (Quoti
 #align quotient_add_group.induction_on QuotientAddGroup.induction_on
 
 @[to_additive]
-instance : CoeTC α (α ⧸ s) :=
+instance : Coe α (α ⧸ s) :=
   ⟨mk⟩
 
 @[to_additive (attr := elab_as_elim)]
diff --git a/Mathlib/RingTheory/Ideal/Quotient.lean b/Mathlib/RingTheory/Ideal/Quotient.lean
index 54806ae56aaf8..84f59450cc93c 100644
--- a/Mathlib/RingTheory/Ideal/Quotient.lean
+++ b/Mathlib/RingTheory/Ideal/Quotient.lean
@@ -104,6 +104,9 @@ def mk (I : Ideal R) : R →+* R ⧸ I where
   map_add' _ _ := rfl
 #align ideal.quotient.mk Ideal.Quotient.mk
 
+instance {I : Ideal R} : Coe R (R ⧸ I) :=
+  ⟨Ideal.Quotient.mk I⟩
+
 /-- Two `RingHom`s from the quotient by an ideal are equal if their
 compositions with `Ideal.Quotient.mk'` are equal.