coprime_of_squarefree_mul

Mathlib.Data.Nat.Squarefree

URI: https://scilib.ai/kg/mathlib#Nat.coprime_of_squarefree_mul

← MathLib Explorer

English

If m n is squarefree, then m and n are coprime.

Русский

Если произведение m и n квадратно свободно, то m и n взаимно простые.

LaTeX

$$$\\\\operatorname{Squarefree}(m n) \\\\Rightarrow \\\\gcd(m,n)=1.$$$

Lean4

theorem coprime_of_squarefree_mul {m n : ℕ} (h : Squarefree (m * n)) : m.Coprime n :=
  coprime_of_dvd fun p hp hm hn => squarefree_iff_prime_squarefree.mp h p hp (mul_dvd_mul hm hn)

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru