Commit 2022-12-14 13:46 2d46f7bd
View on Github →feat port: RingTheory.Coprime.Basic (#899)
a95b16cbade0f938fc24abd05412bde1e84bab9b
Turns out there are actually some more imports needed to port this file which were imported via tactic.ring
in Lean3.