Commit 2025-02-28 15:04 e253d16e

View on Github →

fix: not_prime_zero and not_prime_one Aesop rules (#22394) These rules, which derive a contradiction from Prime 0 or Prime 1, were tagged incorrectly and would therefore add ¬ Prime 0 and ¬ Prime 1 to every goal. Fixes the heartbeat bump introduced in #22334.

Estimated changes

modified theorem Nat.not_prime_one
modified theorem Nat.not_prime_zero
added theorem Nat.prime_one_false
added theorem Nat.prime_zero_false