src/HOL/Number_Theory/Totient.thy
changeset 69096 62a0d10386c1
parent 69064 5840724b1d71
child 69785 9e326f6f8a24