Commit 2024-01-22 09:31 8cab1b0a

View on Github →

feat(Nat/Prime): weaken assumptions in Nat.not_prime_mul (#9901) Assume _ ≠ 1 instead of 1 < _ in Nat.not_prime_mul, Nat.not_prime_mul', Int.not_prime_of_int_mul.

Estimated changes

modified theorem Int.not_prime_of_int_mul
modified theorem Nat.not_prime_mul'
modified theorem Nat.not_prime_mul