Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2018-08-22 19:37 974987ce

View on Github →

refactor(data/nat/prime): cleanup exists_infinite_primes (#271)

  • removing unnecessary initial step
  • giving names to ambiguous copies of this

Estimated changes

modified theorem nat.exists_infinite_primes