IsCoprime_num_den

Stream: Is there code for X?

[Moritz Firsching]

Is there code for the following:

import Mathlib
example (q : ℚ) : Int.gcd q.num q.den = 1 := by sorry

or

example (q : ℚ) : IsCoprime q.num q.den := by sorry

I searched a bit, but only found docs#RatFunc.isCoprime_num_denom.

[Gareth Ma]

If you look at the definition of Rat, you will see that there is a field

reduced : num.natAbs.Coprime den := by decide

So you can use that to derive the exact statement you want :)

[Daniel Weber]

One of docs#Rat 's field seems to be reduced which is what you want

[Gareth Ma]

example (q : ℚ) : IsCoprime q.num q.den := by
  have := q.reduced /- Introduce this into the scope -/
  exact? /- Let the tactics do its magic -/