src/HOL/NumberTheory/Quadratic_Reciprocity.thy
changeset 24077 e7ba448bc571
parent 23431 25ca91279a9b
child 30034 60f64f112174