rw [← this, cast_pow, cast_ofNat]
p : ℕ
hp : p.Prime
this✝¹ : Fact p.Prime
m : ℕ := mersenne p
q : ℕ := m.minFac
hq : q.Prime
this✝ : Fact q.Prime
h_mod_q : q.ModEq (2 ^ p) 1
this : ↑(2 ^ p) = 1
⊢ 2 ^ p = 1
no goals