Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-02-20 01:22 55c9cff7

View on Github →

chore(data/nat/prime): slightly weaken assumption in nat.exists_prime_and_dvd (#12156) It is vacuously true for zero, as everything divides zero.

Estimated changes

Modified src/algebra/squarefree.lean

Modified src/data/nat/prime.lean

modified theorem nat.exists_prime_and_dvd

Modified src/data/pnat/prime.lean

modified theorem pnat.exists_prime_and_dvd

Modified src/ring_theory/int/basic.lean

modified theorem int.exists_prime_and_dvd