Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-09-10 19:00 5e78882f

View on Github →

feat(algebra/parity): Primes are not square (#16430) and a few other basic results about is_square.

Estimated changes

added theorem even.is_square_pow
added theorem even.is_square_zpow
added theorem irreducible.not_square
added theorem is_square.not_prime
added theorem is_square.pow
added theorem is_square.zpow
modified theorem is_square_zero
added theorem prime.not_square