Defs

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

Statistics

Metric	Count
Definitions `succPNat`, `toPNat`, `toPNat'`, `div`, `divExact`, `instInhabited`, `instWellFoundedRelation`, `modDiv`, `modDivAux`, `natPred`, `strongInductionOn`, `instLinearOrderPNat`, `instOfNatPNatOfNeZeroNat`, `instOnePNat`	14
Theorems `canLiftPNat`, `canLiftPNat`, `natPred_succPNat`, `succPNat_coe`, `toPNat'_coe`, `toPNat'_zero`, `pnat`, `coe_eq_one_iff`, `coe_injective`, `coe_le_coe`, `coe_lt_coe`, `coe_toPNat'`, `div_coe`, `eq`, `mk_coe`, `mk_le_mk`, `mk_lt_mk`, `mk_one`, `mod_coe`, `natPred_eq_pred`, `ne_zero`, `not_lt_one`, `one_coe`, `one_le`, `pos`, `succPNat_natPred`, `toPNat'_coe`	27
Total	41

Int

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`canLiftPNat` 📖	mathematical	—	`CanLift` `PNat` `PNat.val`	—	`Nat.toPNat'_coe` `LT.lt.ne'` `LT.lt.le`

Nat

Definitions

Name	Category	Theorems
`succPNat` 📖	CompOp	19 math math: `OrderIso.pnatIsoNat_symm_apply`, `ONote.ofNat_succ`, `succPNat_mono`, `succPNat_le_succPNat`, `PNat.gcd_props`, `PNat.gcd_det_eq`, `Mathlib.Tactic.Ring.instCSLiftValPNatNatSuccPNatHAddOfNat`, `succPNat_coe`, `PNat.succPNat_natPred`, `succPNat_injective`, `Equiv.pnatEquivNat_symm_apply`, `natPred_succPNat`, `succPNat_lt_succPNat`, `PNat.gcd_rel_left'`, `succPNat_strictMono`, `PNat.add_one`, `PNat.gcd_rel_right'`, `succPNat_inj`, `PNat.lt_succ_self`
`toPNat` 📖	CompOp	1 math math: `Mathlib.Tactic.Ring.instCSLiftValPNatNatToPNat`
`toPNat'` 📖	CompOp	6 math math: `toPNat'_coe`, `toPNat'_zero`, `AddChar.val_mem_rootsOfUnity`, `PNat.toPNat'_coe`, `PNat.coe_toPNat'`, `Mathlib.Tactic.Ring.instCSLiftValPNatNatToPNat'HAddPredOfNat`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`canLiftPNat` 📖	mathematical	—	`CanLift` `PNat` `PNat.val`	—	`PNat.toPNat'_coe`
`natPred_succPNat` 📖	mathematical	—	`PNat.natPred` `succPNat`	—	—
`succPNat_coe` 📖	mathematical	—	`PNat.val` `succPNat`	—	—
`toPNat'_coe` 📖	mathematical	—	`PNat.val` `toPNat'`	—	—
`toPNat'_zero` 📖	mathematical	—	`toPNat'` `PNat` `instOfNatPNatOfNeZeroNat`	—	—

NeZero

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`pnat` 📖	mathematical	—	`PNat.val`	—	`PNat.ne_zero`

PNat

Definitions

Name	Category	Theorems
`div` 📖	CompOp	6 math math: `Mathlib.Tactic.Ring.instCSLiftValPNatNatDivExactHAddDivOfNat`, `mod_add_div`, `mod_add_div'`, `div_add_mod`, `div_coe`, `div_add_mod'`
`divExact` 📖	CompOp	2 math math: `Mathlib.Tactic.Ring.instCSLiftValPNatNatDivExactHAddDivOfNat`, `mul_div_exact`
`instInhabited` 📖	CompOp	—
`instWellFoundedRelation` 📖	CompOp	—
`modDiv` 📖	CompOp	—
`modDivAux` 📖	CompOp	1 math math: `modDivAux_spec`
`natPred` 📖	CompOp	13 math math: `natPred_injective`, `Equiv.pnatEquivNat_apply`, `natPred_monotone`, `succPNat_natPred`, `Nat.natPred_succPNat`, `natPred_add_one`, `one_add_natPred`, `OrderIso.pnatIsoNat_apply`, `natPred_inj`, `natPred_strictMono`, `natPred_lt_natPred`, `natPred_le_natPred`, `natPred_eq_pred`
`strongInductionOn` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coe_eq_one_iff` 📖	mathematical	—	`val` `PNat` `instOfNatPNatOfNeZeroNat`	—	`Subtype.coe_injective` `one_coe`
`coe_injective` 📖	mathematical	—	`PNat` `val`	—	`Subtype.coe_injective`
`coe_le_coe` 📖	mathematical	—	`val` `PNat` `Preorder.toLE` `PartialOrder.toPreorder` `LinearOrder.toPartialOrder` `instLinearOrderPNat`	—	—
`coe_lt_coe` 📖	mathematical	—	`val` `PNat` `Preorder.toLT` `PartialOrder.toPreorder` `LinearOrder.toPartialOrder` `instLinearOrderPNat`	—	—
`coe_toPNat'` 📖	mathematical	—	`Nat.toPNat'` `val`	—	`eq` `toPNat'_coe` `pos`
`div_coe` 📖	mathematical	—	`div` `val`	—	—
`eq` 📖	—	`val`	—	—	—
`mk_coe` 📖	mathematical	—	`val`	—	—
`mk_le_mk` 📖	—	—	—	—	—
`mk_lt_mk` 📖	—	—	—	—	—
`mk_one` 📖	mathematical	—	`PNat` `instOfNatPNatOfNeZeroNat`	—	—
`mod_coe` 📖	mathematical	—	`val` `mod`	—	—
`natPred_eq_pred` 📖	mathematical	—	`natPred`	—	—
`ne_zero` 📖	—	—	—	—	`LT.lt.ne'`
`not_lt_one` 📖	mathematical	—	`PNat` `Preorder.toLT` `PartialOrder.toPreorder` `LinearOrder.toPartialOrder` `instLinearOrderPNat` `instOfNatPNatOfNeZeroNat`	—	`not_lt_of_ge` `one_le`
`one_coe` 📖	mathematical	—	`val` `PNat` `instOfNatPNatOfNeZeroNat`	—	—
`one_le` 📖	mathematical	—	`PNat` `Preorder.toLE` `PartialOrder.toPreorder` `LinearOrder.toPartialOrder` `instLinearOrderPNat` `instOfNatPNatOfNeZeroNat`	—	—
`pos` 📖	mathematical	—	`val`	—	—
`succPNat_natPred` 📖	mathematical	—	`Nat.succPNat` `natPred`	—	—
`toPNat'_coe` 📖	mathematical	—	`val` `Nat.toPNat'`	—	—

(root)

Definitions

Name	Category	Theorems
`instLinearOrderPNat` 📖	CompOp	75 math math: `PNat.bot_eq_one`, `PNat.addLeftMono`, `OrderIso.pnatIsoNat_symm_apply`, `PNat.map_subtype_embedding_Ico`, `Nat.succPNat_mono`, `PNat.find_le`, `Nat.succPNat_le_succPNat`, `PNat.Icc_eq_finset_subtype`, `PNat.Ioo_eq_finset_subtype`, `PNat.instIsOrderedCancelMonoid`, `PNat.le_of_dvd`, `PNat.card_Icc`, `PNat.tendsto_comp_val_iff`, `PNat.lt_add_right`, `PNat.find_mono`, `ADEInequality.lt_six`, `PNat.not_lt_one`, `PNat.Ico_eq_finset_subtype`, `PNat.sub_coe`, `PNat.addLeftReflectLT`, `PNat.natPred_monotone`, `PNat.ofNat_lt_ofNat`, `tendsto_PNat_val_atTop_atTop`, `PNat.coe_le_coe`, `PNat.find_le_iff`, `PNat.card_fintype_uIcc`, `PNat.map_subtype_embedding_Icc`, `PNat.uIcc_eq_finset_subtype`, `PNat.ofNat_le_ofNat`, `PNat.equivNonZeroDivisorsNat_symm_apply_coe`, `Nat.succPNat_lt_succPNat`, `Nat.succPNat_strictMono`, `PNat.add_one_le_iff`, `PNat.card_Ico`, `PNat.map_subtype_embedding_Ioo`, `PNat.Ioc_eq_finset_subtype`, `PNat.find_lt_iff`, `PNat.succ_eq_add_one`, `PNat.map_subtype_embedding_uIcc`, `LucasLehmer.two_lt_q`, `PNat.addLeftReflectLE`, `PNat.card_fintype_Ioo`, `PNat.Prime.one_lt`, `PNat.card_uIcc`, `OrderIso.pnatIsoNat_apply`, `PNat.instWellFoundedLT`, `PNat.lt_add_left`, `PNat.sub_le`, `PNat.card_Ioo`, `PNat.equivNonZeroDivisorsNat_apply_coe`, `PNat.card_fintype_Ioc`, `PNat.card_fintype_Ico`, `PNat.find_min'`, `Complex.UnitDisc.tendsto_pow_atTop_nhds_zero`, `PNat.natPred_strictMono`, `PNat.natPred_lt_natPred`, `PNat.instNoMaxOrder`, `PNat.lt_add_one_iff`, `PNat.card_Ioc`, `PNat.natPred_le_natPred`, `EisensteinSeries.tendsto_tsum_one_div_linear_sub_succ_eq`, `PNat.lt_find_iff`, `Mathlib.Tactic.PNatToNat.coe_le_coe`, `PNat.le_one_iff`, `PNat.coe_lt_coe`, `Mathlib.Tactic.PNatToNat.coe_lt_coe`, `PNat.map_subtype_embedding_Ioc`, `PNat.one_le`, `PNat.card_fintype_Icc`, `PNat.one_le_find`, `PNat.mod_le`, `PNat.addLeftStrictMono`, `PNat.le_find_iff`, `PNat.lt_succ_self`, `tendsto_zero_geometric_tsum_pnat`
`instOfNatPNatOfNeZeroNat` 📖	CompOp	50 math math: `PNat.bot_eq_one`, `PNat.mk_one`, `PNat.coe_eq_one_iff`, `Rat.pnatDen_one`, `PNat.not_lt_one`, `PNat.Prime.not_dvd_one`, `PNat.one_coprime`, `PNat.dvd_one_iff`, `PNat.le_sub_one_of_lt`, `PNat.not_prime_one`, `Nat.toPNat'_zero`, `PNat.one_coe`, `PNat.fact_prime_two`, `PNat.add_one_le_iff`, `PNat.one_gcd`, `PNat.prime_five`, `PNat.recOn_succ`, `divisorsAntidiagonalFactors_one`, `ppow_one`, `PNat.prime_two`, `PNat.succ_eq_add_one`, `LucasLehmer.two_lt_q`, `PNat.mk_ofNat`, `PNat.Prime.one_lt`, `ADEInequality.admissible_E'4`, `PNat.fact_prime_five`, `PNat.dvd_prime`, `PNat.coprime_one`, `PNat.gcd_one`, `PNat.find_eq_one`, `PNat.factorMultiset_one`, `PNat.add_one`, `ADEInequality.admissible_E'5`, `PNat.fact_prime_three`, `PrimeMultiset.prod_zero`, `PNat.lt_add_one_iff`, `ADEInequality.lt_three`, `ONote.scale_eq_mul`, `PNat.le_one_iff`, `PNat.one_le`, `PNat.isCoprime_iff`, `PNat.one_lt_of_lt`, `PNat.one_le_find`, `Rat.pnatDen_zero`, `PNatPowAssoc.ppow_one`, `ADEInequality.admissible_E'3`, `PNat.prime_three`, `PNat.recOn_one`, `PNat.exists_eq_succ_of_ne_one`, `EqualCharZero.pnatCast_one`
`instOnePNat` 📖	CompOp	1 math math: `PrimeMultiset.prod_ofPNatList`

---

← Back to Index