FormalConjecturesForMathlib/Data/Nat/Prime/Infinite.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Imports (1)
Imported by 1 file
  1. lemma Nat.exists_prime_not_dvd line 22 source

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: Nat, Ne, OfNat.ofNat, Exists, And, Nat.Prime, Not, Dvd.dvd

    Proof uses: LE.le, HAdd.hAdd, Nat.exists_infinite_primes, Exists.intro, And.intro, Nat.not_dvd_of_pos_of_lt

    10 instances, coercions and auxiliary constants left out.

    Tactic trace: 4 steps

    Open to load the checked before-and-after goal states.