feat(algebra/parity): Primes are not square (#16430)
feat(algebra/parity): Primes are not square (#16430)

and a few other basic results about `is_square`.





leanprover-community/mathlib,leanprover-community/mathlib