isPrime

write a function isPrime that given a natural number a, returns true if and only if a is prime.

Function Signature

import Mathlib.Data.Nat.Prime.Defs

def isPrime(a: Nat): Bool

Theorem Signature

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

View All Submissions

Please log in or register to submit a solution for this challenge.