isCoprime_num_denom — Mathlib

English

For any x, the numerator and denominator are coprime: IsCoprime(x.num, x.denom).

Русский

Для любой x числитель и знаменатель взаимно просты: IsCoprime(x.num, x.denom).

LaTeX

$$$\operatorname{IsCoprime}(\operatorname{num}(x),\operatorname{denom}(x))$$$

Lean4

theorem isCoprime_num_denom (x : RatFunc K) : IsCoprime x.num x.denom := by
  classical
  induction x using RatFunc.induction_on with
  | _ p q hq
  rw [num_div, denom_div _ hq]
  exact
    (isCoprime_mul_unit_left ((leadingCoeff_ne_zero.2 <| right_div_gcd_ne_zero hq).isUnit.inv.map C) _ _).2
      (isCoprime_div_gcd_div_gcd hq)

Похожие утверждения