Equiv

📁 Source: Mathlib/Data/PNat/Equiv.lean

Statistics

Metric	Count
Definitions pnatEquivNat	1
Theorems pnatEquivNat_apply, pnatEquivNat_symm_apply	2
Total	3

Equiv

Definitions

Name	Category	Theorems
pnatEquivNat 📖	CompOp	2 math math: pnatEquivNat_apply, pnatEquivNat_symm_apply

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
pnatEquivNat_apply 📖	mathematical	—	DFunLike.coe Equiv PNat EquivLike.toFunLike instEquivLike pnatEquivNat PNat.natPred	—	—
pnatEquivNat_symm_apply 📖	mathematical	—	DFunLike.coe Equiv PNat EquivLike.toFunLike instEquivLike symm pnatEquivNat Nat.succPNat	—	—

---

← Back to Index