English
If n ≠ m, then cyclotomic(n, ℚ) and cyclotomic(m, ℚ) are coprime polynomials.
Русский
Если n ≠ m, то cyclotomic(n, ℚ) и cyclotomic(m, ℚ) взаимно простые полиномы.
LaTeX
$$$$ \\operatorname{IsCoprime}(\\operatorname{cyclotomic}(n, \\mathbb{Q}), \\operatorname{cyclotomic}(m, \\mathbb{Q})). $$$$
Lean4
/-- If `n ≠ m`, then `(cyclotomic n ℚ)` and `(cyclotomic m ℚ)` are coprime. -/
theorem isCoprime_rat {n m : ℕ} (h : n ≠ m) : IsCoprime (cyclotomic n ℚ) (cyclotomic m ℚ) :=
by
rcases n.eq_zero_or_pos with (rfl | hnzero)
· exact isCoprime_one_left
rcases m.eq_zero_or_pos with (rfl | hmzero)
· exact isCoprime_one_right
rw [Irreducible.coprime_iff_not_dvd <| cyclotomic.irreducible_rat <| hnzero]
exact fun hdiv =>
h <|
cyclotomic_injective <|
eq_of_monic_of_associated (cyclotomic.monic n ℚ) (cyclotomic.monic m ℚ) <|
Irreducible.associated_of_dvd (cyclotomic.irreducible_rat hnzero) (cyclotomic.irreducible_rat hmzero) hdiv
