case h₁
p : ℕ
⊢ minFac (2 ^ p - 1) ∣ 2 ^ p - 1
p : ℕ
⊢ ↑(mersenne p) = 0
ext <;> simp [mersenne, q, ZMod.nat_cast_zmod_eq_zero_iff_dvd, -pow_pos]
no goals
case h₁
p : ℕ
⊢ minFac (2 ^ p - 1) ∣ 2 ^ p - 1
apply Nat.minFac_dvd