src/HOL/Number_Theory/Totient.thy
changeset 69764 3ceff650adb9
parent 69064 5840724b1d71
child 69785 9e326f6f8a24