decidableProbablePrime

Mathlib.NumberTheory.FermatPsp

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

English

If n is a FermatPsp to base b, then n and b are coprime (assuming b ≥ 1).

Русский

Если n является псевдопростым Ферматo по основанию b, то n и b взаимно просты (при b ≥ 1).

LaTeX

$$Nat.Coprime\$n,b\$ given FermatPsp(n,b)$$

Lean4

instance decidableProbablePrime (n b : ℕ) : Decidable (ProbablePrime n b) :=
  Nat.decidable_dvd _ _

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

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

Разделы

Аффилиация

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