coprime_num_den — Mathlib

English

For every q ∈ ℚ≥0, the numerator and denominator are coprime: q.num and q.den share no common positive divisor.

Русский

Пусть q ∈ ℚ≥0. Числитель q.num и знаменатель q.den взаимно просты.

LaTeX

$$$ q.num.Coprime q.den $$$

Lean4

theorem coprime_num_den (q : ℚ≥0) : q.num.Coprime q.den := by
  simpa [num, den] using
    Rat.reduced
      _
        -- TODO: Rename `Rat.coe_nat_num`, `Rat.intCast_den`, `Rat.ofNat_num`, `Rat.ofNat_den`

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