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