Nat

📁 Source: Mathlib/Logic/Equiv/Nat.lean

Statistics

Metric	Count
Definitions boolProdNatEquivNat, intEquivNat, natSumNatEquivNat, prodEquivOfEquivNat	4
Theorems boolProdNatEquivNat_apply, boolProdNatEquivNat_symm_apply, natSumNatEquivNat_apply, natSumNatEquivNat_symm_apply	4
Total	8

Equiv

Definitions

Name	Category	Theorems
boolProdNatEquivNat 📖	CompOp	2 math math: boolProdNatEquivNat_symm_apply, boolProdNatEquivNat_apply
intEquivNat 📖	CompOp	—
natSumNatEquivNat 📖	CompOp	2 math math: natSumNatEquivNat_symm_apply, natSumNatEquivNat_apply
prodEquivOfEquivNat 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
boolProdNatEquivNat_apply 📖	mathematical	—	DFunLike.coe Equiv EquivLike.toFunLike instEquivLike boolProdNatEquivNat Nat.bit	—	—
boolProdNatEquivNat_symm_apply 📖	mathematical	—	DFunLike.coe Equiv EquivLike.toFunLike instEquivLike symm boolProdNatEquivNat Nat.boddDiv2	—	—
natSumNatEquivNat_apply 📖	mathematical	—	DFunLike.coe Equiv EquivLike.toFunLike instEquivLike natSumNatEquivNat	—	—
natSumNatEquivNat_symm_apply 📖	mathematical	—	DFunLike.coe Equiv EquivLike.toFunLike instEquivLike symm natSumNatEquivNat Nat.bodd Nat.div2	—	—

---

← Back to Index