decidablePsp

Mathlib.NumberTheory.FermatPsp

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

English

ProbablePrime n b iff b^(n-1) ≡ 1 (mod n).

Русский

Вероятно простое n по основанию b эквивалентно b^(n-1) ≡ 1 (mod n).

LaTeX

$$ProbablePrime\$n,b\$ \\iff b^{(n-1)} \\equiv 1 \\,[\\!\\!\\! {n}]$$

Lean4

instance decidablePsp (n b : ℕ) : Decidable (FermatPsp n b) :=
  inferInstanceAs (Decidable (_ ∧ _))

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

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

Разделы

Аффилиация

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