src/HOL/Number_Theory/Modular_Inverse.thy
changeset 82733 8b537e1af2ec
parent 82518 da14e77a48b2