Mathlib v3 is deprecated. Go to Mathlib v4

Theorem int.exists_prime_and_dvd

Modification history

2022-02-20 01:22

src/ring_theory/int/basic.lean

chore(data/nat/prime): slightly weaken assumption in nat.exists_prime_and_dvd (#12156) …

Modified int.exists_prime_and_dvd View on Github →

2021-12-18 14:23

src/ring_theory/int/basic.lean

feat(data/int): various lemmas (#10862)

Added int.exists_prime_and_dvd View on Github →