theorem
proved
term proof
mod6_thirteen_prime
show as:
view Lean formalization →
formal statement (Lean)
1861theorem mod6_thirteen_prime : Prime 13 ∧ 13 % 6 = 1 := by native_decide
proof body
Term-mode proof.
1862
1863/-- 19 ≡ 1 (mod 6). -/