of_squarefree_mul — Mathlib

English

If the product m n is squarefree in a commutative monoid, then m and n are relatively prime: any common divisor is a unit.

Русский

Если произведение m n квадратно свободно в коммутативном моноиде, то m и n взаимно просты: любой общий делитель является единицей.

LaTeX

$$[CommMonoid R] {m n : R} (h : Squarefree (m * n)) : IsRelPrime m n$$

Lean4

theorem of_squarefree_mul [CommMonoid R] {m n : R} (h : Squarefree (m * n)) : IsRelPrime m n := fun c hca hcb ↦
  h c (mul_dvd_mul hca hcb)

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