Closed seewoo5 closed 2 weeks ago
IsCoprime.num_denom
isCoprime_num_denom
https://github.com/leanprover-community/mathlib4/blob/c95b27fcb89ed1932c9c0d70585904a62472d435/Mathlib/FieldTheory/RatFunc/Basic.lean#L1013
oops I'm dumb
seewoo5
commented
2 weeks ago seewoo5
commented
2 weeks ago
IsCoprime.num_denomwithisCoprime_num_denombelowhttps://github.com/leanprover-community/mathlib4/blob/c95b27fcb89ed1932c9c0d70585904a62472d435/Mathlib/FieldTheory/RatFunc/Basic.lean#L1013