modInv

write a function that given a natrual number a and a prime number p, returns a natural number x such that (a*x)%p=1. if no solution exists, return none.

Function Signature

import Mathlib.Data.Prime.Defs

def modInv(a: Nat) (p:Nat)(hp:p.Prime): Option Nat

Theorem Signature

theorem modInv_correct(a:Nat) (p:Nat)(hp:p.Prime):
  (∃ x:Nat, (a*x)%p=1)->(a*(modInv a p hp).get!)%p=1

Additional Theorem Signature

theorem modInv_none(a:Nat) (p:Nat)(hp:p.Prime): (Not (∃ x, (a*x)%p=1))-> modInv a p hp=none

View All Submissions

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