probablePrime_iff_modEq — Mathlib

English

ProbablePrime n b ⇔ b^(n−1) ≡ 1 (mod n) when b ≥ 1.

Русский

ProbablePrime n b эквивалентно b^(n−1) ≡ 1 (mod n) при b ≥ 1.

LaTeX

$$ProbablePrime\$n,b\$ \\iff b^{(n-1)} \\equiv 1 \\pmod{n}$$

Lean4

theorem probablePrime_iff_modEq (n : ℕ) {b : ℕ} (h : 1 ≤ b) : ProbablePrime n b ↔ b ^ (n - 1) ≡ 1 [MOD n] :=
  by
  have : 1 ≤ b ^ (n - 1) := one_le_pow₀ h
  rw [Nat.ModEq.comm]
  constructor
  · intro h₁
    apply Nat.modEq_of_dvd
    exact mod_cast h₁
  · intro h₁
    exact mod_cast Nat.ModEq.dvd h₁

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