feat: add a coe to ideal quotient rings (#6620)

Like we have for (Add)Subgroups already
leanprover-community · Aug 23, 2023 · 330b78e · 330b78e
1 parent 23e7b3d
commit 330b78e
Show file tree

Hide file tree

Showing 2 changed files with 4 additions and 1 deletion.
diff --git 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
@@ -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.