PNatToNat

📁 Source: Mathlib/Tactic/PNatToNat.lean

Statistics

Metric	Count
Definitions tacticPnat_positivity, tacticPnat_to_nat	2
Theorems coe_inj, coe_le_coe, coe_lt_coe, sub_coe	4
Total	6

Mathlib.Tactic.PNatToNat

Definitions

Name	Category	Theorems
tacticPnat_positivity 📖	CompOp	—
tacticPnat_to_nat 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coe_inj 📖	mathematical	—	PNat.val	—	—
coe_le_coe 📖	mathematical	—	PNat Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder instLinearOrderPNat PNat.val	—	—
coe_lt_coe 📖	mathematical	—	PNat Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder instLinearOrderPNat PNat.val	—	—
sub_coe 📖	mathematical	—	PNat.val PNat PNat.instSub	—	PNat.sub_coe

---

← Back to Index