Dedekind Integers form a Ring

Stream: maths

[Alexander Kurz]

As an exercise, I want to prove that the Dedekind Integers form a Ring. A Dedekind Integer is a pair (p,n) of natural numbers and two pairs are equivalent if (p+n'=p'+n). I can define all of this, but when I want to show that the Dedekind Integers are an instance of Ring https://leanprover-community.github.io/mathlib4_docs/Mathlib/Algebra/Ring/Defs.html#Ring then I need to match up the equality of Ring with the equivalence of my integers. I did show that my integers are an instance of Setoid, but I dont know how to go on from there. How do I match up the equality of Ring with the equivalence relation that I defined for my integers?

[Kevin Buzzard]

Spoiler alert: your question is presumably answered in this file.

[Kevin Buzzard]

Maybe the answer to your question is abbrev MyInt := Quotient R_equiv (line 119)? It's difficult to give you a good answer because you did not ask your question in the form of a #mwe . If you write code and ask questions like "how to fill in this sorry" then it's much easier to help.

[Alexander Kurz]

Thanks, taking a quotient sounds good to me. I will try that.