PNat

📁 Source: Mathlib/Algebra/Order/Monoid/PNat.lean

Statistics

Metric	Count
Definitions equivNonZeroDivisorsNat	1
Theorems equivNonZeroDivisorsNat_apply_coe, equivNonZeroDivisorsNat_symm_apply_coe	2
Total	3

PNat

Definitions

Name	Category	Theorems
equivNonZeroDivisorsNat 📖	CompOp	2 math math: equivNonZeroDivisorsNat_symm_apply_coe, equivNonZeroDivisorsNat_apply_coe

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
equivNonZeroDivisorsNat_apply_coe 📖	mathematical	—	Submonoid MulZeroOneClass.toMulOneClass MonoidWithZero.toMulZeroOneClass Nat.instMonoidWithZero SetLike.instMembership Submonoid.instSetLike nonZeroDivisors DFunLike.coe OrderMonoidIso PNat PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder instLinearOrderPNat Subtype.preorder Nat.instPreorder instMulPNat Submonoid.mul EquivLike.toFunLike OrderMonoidIso.instEquivLike equivNonZeroDivisorsNat val	—	—
equivNonZeroDivisorsNat_symm_apply_coe 📖	mathematical	—	DFunLike.coe OrderMonoidIso Submonoid MulZeroOneClass.toMulOneClass MonoidWithZero.toMulZeroOneClass Nat.instMonoidWithZero SetLike.instMembership Submonoid.instSetLike nonZeroDivisors PNat Subtype.preorder Nat.instPreorder PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder instLinearOrderPNat Submonoid.mul instMulPNat EquivLike.toFunLike OrderMonoidIso.instEquivLike OrderMonoidIso.symm equivNonZeroDivisorsNat	—	—

---

← Back to Index