src/HOL/NumberTheory/Quadratic_Reciprocity.thy
changeset 29270 0eade173f77e
parent 23431 25ca91279a9b
child 30034 60f64f112174