The primes as a subtype: the Fact instance

Mathlib's Nat.Primes is the subtype of prime natural numbers. Much of the prime-indexed API (ZMod p as a field, the p-adic integers ℤ_[p], Sylow theory) takes its prime as a natural number p : ℕ together with an instance [Fact p.Prime], so a family indexed by Nat.Primes, such as ∀ p : Nat.Primes, ℤ_[p], can only be written once the primality of (p : ℕ) is available to instance search. Mathlib supplies it only as a local instance (Mathlib/NumberTheory/Padics/HeightOneSpectrum.lean); this module makes it global.

Main declarations

• Nat.Primes.instFactPrime: for p : Nat.Primes, the instance Fact (p : ℕ).Prime.

instance Nat.Primes.instFactPrime (p : Primes) : Fact (Prime ↑p)

A prime, as an element of the subtype Nat.Primes, is prime: the Fact instance under which the prime-indexed API, for instance the p-adic integers ℤ_[p], can be used for p : Nat.Primes.