Theorems · Definition · number theory
Nat.Prime
ℕ → Prop
Nat.Prime p means that p is a prime number, that is, a natural number
at least 2 whose only divisors are p and 1.
The theorem Nat.prime_def witnesses this description of a prime number.
- Defined in
- Mathlib.Data.Nat.Prime.Defs
- Cited by
- 2,059 results in Mathlib
- Foundations
- Depth 19 from the axioms, rests on 105 definitions · uses propext
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites1
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Irreducibleproof · cited by 496
Cited by2,294
Results whose statement or proof uses this declaration.
- Nat.factorizationproof · cited by 215
- PadicIntstatement and proof · cited by 179
- Padicstatement and proof · cited by 151
- Nat.Prime.one_ltstatement · cited by 118
- Nat.Prime.ne_zerostatement and proof · cited by 109
- Nat.Prime.posstatement and proof · cited by 83
- Nat.Primesproof · cited by 63
- Nat.Prime.ne_onestatement and proof · cited by 61
- Nat.prime_twostatement · cited by 55
- Nat.Prime.two_lestatement and proof · cited by 53
- legendreSymstatement and proof · cited by 51
- Perfection.coeffstatement and proof · cited by 51
Showing the 200 most cited of 2,294.