Submission Details

Back to Submissions List

Challenge: isPrime

Submitted by: Command Master

Submitted at: 2024-11-15 12:02:28

Code:

import Mathlib.Data.Nat.Prime.Defs

def isPrime(a: Nat): Bool

:= decide (Nat.Prime a)

First Theorem Proof:

theorem isPrime_correct(a: Nat): (isPrime a)=True <-> Nat.Prime a

:= by simp [isPrime]

Status: Correct

Feedback: