pairwise_coprime_fermatNumber — Mathlib

English

The family {F_n} is pairwise coprime: any two distinct Fermat numbers are coprime.

Русский

Семейство {F_n} попарно взаимно простое: любые два разных числа Ферма взаимно просты.

LaTeX

$$Pairwise\$ \\mathrm{fermatNumber}(m) , \\mathrm{fermatNumber}(n) \$$$

Lean4

theorem pairwise_coprime_fermatNumber : Pairwise fun m n ↦ Coprime (fermatNumber m) (fermatNumber n) := fun _m _n ↦
  coprime_fermatNumber_fermatNumber

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