coprime_div_gcd_of_squarefree — Mathlib

English

Let m be squarefree and n ≠ 0. Then Coprime (m / gcd(m,n)) n.

Русский

Пусть m квадратно свободно, n ≠ 0. Тогда модуля m / gcd(m,n) и n взаимно просты.

LaTeX

$$$\\\\operatorname{Squarefree}(m) \\\\land n \\neq 0 \\\\Rightarrow \\\\gcd\\left(\\\\frac{m}{\\\\gcd(m,n)},\, n\\\\right) = 1.$$$

Lean4

theorem coprime_div_gcd_of_squarefree (hm : Squarefree m) (hn : n ≠ 0) : Coprime (m / gcd m n) n :=
  by
  have : Coprime (m / gcd m n) (gcd m n) := coprime_of_squarefree_mul <| by simpa [Nat.div_mul_cancel, gcd_dvd_left]
  simpa [Nat.div_mul_cancel, gcd_dvd_right] using
    (coprime_div_gcd_div_gcd (m := m) (gcd_ne_zero_right hn).bot_lt).mul_right this

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