theorem
proved
term proof
mod4_fortyseven_prime
show as:
view Lean formalization →
formal statement (Lean)
1619theorem mod4_fortyseven_prime : Prime 47 ∧ 47 % 4 = 3 := by native_decide
proof body
Term-mode proof.
1620
1621/-- 59 ≡ 3 (mod 4). -/