Mathlib Map

Theorems · Definition · number theory

Nat.succPNat

ℕ → ℕ+

Write a successor as an element of ℕ+.

Defined in
Mathlib.Data.PNat.Defs
Cited by
29 results in Mathlib
Foundations
Depth 11 from the axioms · uses no axioms
Mathlib docsSourceLoogleLeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Equiv.pnatEquivNat · cited by 8Equiv.pnatEquivNatPNat.gcd_props · cited by 8PNat.gcd_propsONote.ofNat · cited by 8ONote.ofNatPNat.XgcdType.w · cited by 6XgcdType.wPNat.XgcdType.z · cited by 6XgcdType.zNat.toPNat' · cited by 6Nat.toPNat'PNat.gcdA' · cited by 6PNat.gcdA'PNat.gcdB' · cited by 6PNat.gcdB'PNat.XgcdType.b · cited by 6XgcdType.bONote.fundamentalSequence_has_prop · cited by 5ONote.fundamentalSequence…PNat.XgcdType.a · cited by 5XgcdType.aNat.succPNat_strictMono · cited by 4Nat.succPNat_strictMonoPNat.gcd_eq · cited by 4PNat.gcd_eqONote.repr_ofNat · cited by 3ONote.repr_ofNatONote.mulNat · cited by 3ONote.mulNatPNat · cited by 392PNatNat.succPNatCITED BYCITES

Cites1

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

  • PNatstatement · cited by 392

Cited by42

Results whose statement or proof uses this declaration.