Basic

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

Statistics

Metric	Count
Definitions `pnatIsoNat`, `caseStrongInductionOn`, `coeAddHom`, `coeMonoidHom`, `instCancelCommMonoid`, `instCommMonoid`, `instOrderBot`, `instSub`, `recOn`, `instAddCommSemigroupPNat`, `instAddLeftCancelSemigroupPNat`, `instAddPNat`, `instAddRightCancelSemigroupPNat`, `instDistribPNat`, `instMulPNat`	15
Theorems `succPNat_inj`, `succPNat_injective`, `succPNat_le_succPNat`, `succPNat_lt_succPNat`, `succPNat_mono`, `succPNat_strictMono`, `pnatIsoNat_apply`, `pnatIsoNat_symm_apply`, `addLeftMono`, `addLeftReflectLE`, `addLeftReflectLT`, `addLeftStrictMono`, `add_coe`, `add_one`, `add_one_le_iff`, `add_sub`, `add_sub_of_lt`, `bot_eq_one`, `coeAddHom_apply`, `coe_coeMonoidHom`, `coe_inj`, `div_add_mod`, `div_add_mod'`, `dvd_antisymm`, `dvd_iff`, `dvd_iff'`, `dvd_one_iff`, `exists_eq_succ_of_ne_one`, `instIsOrderedCancelMonoid`, `instWellFoundedLT`, `le_of_dvd`, `le_one_iff`, `le_sub_one_of_lt`, `lt_add_left`, `lt_add_one_iff`, `lt_add_right`, `lt_succ_self`, `mk_ofNat`, `modDivAux_spec`, `mod_add_div`, `mod_add_div'`, `mod_le`, `mul_coe`, `mul_div_exact`, `natPred_add_one`, `natPred_inj`, `natPred_injective`, `natPred_le_natPred`, `natPred_lt_natPred`, `natPred_monotone`, `natPred_strictMono`, `ofNat_inj`, `ofNat_le_ofNat`, `ofNat_lt_ofNat`, `one_add_natPred`, `one_lt_of_lt`, `pos_of_div_pos`, `pow_coe`, `recOn_one`, `recOn_succ`, `sub_add_of_lt`, `sub_coe`, `sub_le`, `val_ofNat`	64
Total	79

Nat

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`succPNat_inj` 📖	mathematical	—	`succPNat`	—	`succPNat_injective`
`succPNat_injective` 📖	mathematical	—	`PNat` `succPNat`	—	`StrictMono.injective` `succPNat_strictMono`
`succPNat_le_succPNat` 📖	mathematical	—	`PNat` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `instLinearOrderPNat` `succPNat`	—	`StrictMono.le_iff_le` `succPNat_strictMono`
`succPNat_lt_succPNat` 📖	mathematical	—	`PNat` `Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `instLinearOrderPNat` `succPNat`	—	`StrictMono.lt_iff_lt` `succPNat_strictMono`
`succPNat_mono` 📖	mathematical	—	`Monotone` `PNat` `instPreorder` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `instLinearOrderPNat` `succPNat`	—	`StrictMono.monotone` `succPNat_strictMono`
`succPNat_strictMono` 📖	mathematical	—	`StrictMono` `PNat` `instPreorder` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `instLinearOrderPNat` `succPNat`	—	—

OrderIso

Definitions

Name	Category	Theorems
`pnatIsoNat` 📖	CompOp	2 math math: `pnatIsoNat_symm_apply`, `pnatIsoNat_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`pnatIsoNat_apply` 📖	mathematical	—	`DFunLike.coe` `RelIso` `PNat` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `instLinearOrderPNat` `RelIso.instFunLike` `pnatIsoNat` `PNat.natPred`	—	—
`pnatIsoNat_symm_apply` 📖	mathematical	—	`DFunLike.coe` `OrderIso` `PNat` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `instLinearOrderPNat` `instFunLikeOrderIso` `symm` `pnatIsoNat` `Nat.succPNat`	—	—

PNat

Definitions

Name	Category	Theorems
`caseStrongInductionOn` 📖	CompOp	—
`coeAddHom` 📖	CompOp	1 math math: `coeAddHom_apply`
`coeMonoidHom` 📖	CompOp	1 math math: `coe_coeMonoidHom`
`instCancelCommMonoid` 📖	CompOp	—
`instCommMonoid` 📖	CompOp	27 math math: `instIsOrderedCancelMonoid`, `PrimeMultiset.prod_dvd_prod`, `factorMultiset_le_iff`, `PrimeMultiset.prod_dvd_iff'`, `Prime.not_dvd_one`, `dvd_lcm_right`, `gcd_dvd_right`, `dvd_one_iff`, `gcd_eq_right_iff_dvd`, `count_factorMultiset`, `factorMultiset_le_iff'`, `dvd_iff`, `exists_prime_and_dvd`, `PrimeMultiset.prod_dvd_iff`, `dvd_lcm_left`, `PrimeMultiset.prod_ofPNatMultiset`, `gcd_dvd_left`, `dvd_prime`, `factorMultiset_pow`, `pow_coe`, `dvd_iff'`, `Mathlib.Tactic.Ring.instCSLiftValPNatNatHPow`, `mem_factorMultiset`, `PrimeMultiset.prod_smul`, `Finset.PNat.coe_prod`, `gcd_eq_left_iff_dvd`, `coe_coeMonoidHom`
`instOrderBot` 📖	CompOp	1 math math: `bot_eq_one`
`instSub` 📖	CompOp	7 math math: `Mathlib.Tactic.PNatToNat.sub_coe`, `sub_coe`, `add_sub`, `le_sub_one_of_lt`, `sub_add_of_lt`, `sub_le`, `add_sub_of_lt`
`recOn` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`addLeftMono` 📖	mathematical	—	`AddLeftMono` `PNat` `instAddPNat` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `instLinearOrderPNat`	—	`Positive.addLeftMono` `IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid`
`addLeftReflectLE` 📖	mathematical	—	`AddLeftReflectLE` `PNat` `instAddPNat` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `instLinearOrderPNat`	—	`Positive.addLeftReflectLE` `IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT` `contravariant_lt_of_covariant_le`
`addLeftReflectLT` 📖	mathematical	—	`AddLeftReflectLT` `PNat` `instAddPNat` `Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `instLinearOrderPNat`	—	`Positive.addLeftReflectLT` `IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `contravariant_lt_of_covariant_le`
`addLeftStrictMono` 📖	mathematical	—	`AddLeftStrictMono` `PNat` `instAddPNat` `Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `instLinearOrderPNat`	—	`Positive.addLeftStrictMono` `IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid`
`add_coe` 📖	mathematical	—	`val` `PNat` `instAddPNat`	—	—
`add_one` 📖	mathematical	—	`PNat` `instAddPNat` `instOfNatPNatOfNeZeroNat` `Nat.succPNat` `val`	—	—
`add_one_le_iff` 📖	mathematical	—	`PNat` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `instLinearOrderPNat` `instAddPNat` `instOfNatPNatOfNeZeroNat` `Preorder.toLT`	—	—
`add_sub` 📖	mathematical	—	`PNat` `instSub` `instAddPNat`	—	`add_right_cancel` `AddRightCancelSemigroup.toIsRightCancelAdd` `sub_add_of_lt` `lt_add_left`
`add_sub_of_lt` 📖	mathematical	`PNat` `Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `instLinearOrderPNat`	`instAddPNat` `instSub`	—	`eq` `add_coe` `sub_coe` `add_tsub_cancel_of_le` `CanonicallyOrderedAdd.toExistsAddOfLE` `Nat.instCanonicallyOrderedAdd` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `Nat.instOrderedSub` `LT.lt.le`
`bot_eq_one` 📖	mathematical	—	`Bot.bot` `PNat` `OrderBot.toBot` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `instLinearOrderPNat` `instOrderBot` `instOfNatPNatOfNeZeroNat`	—	—
`coeAddHom_apply` 📖	mathematical	—	`DFunLike.coe` `AddHom` `PNat` `instAddPNat` `AddHom.funLike` `coeAddHom` `val`	—	—
`coe_coeMonoidHom` 📖	mathematical	—	`DFunLike.coe` `MonoidHom` `PNat` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `CommMonoid.toMonoid` `instCommMonoid` `Nat.instMulOneClass` `MonoidHom.instFunLike` `coeMonoidHom` `val`	—	—
`coe_inj` 📖	mathematical	—	`val`	—	`SetCoe.ext_iff`
`div_add_mod` 📖	mathematical	—	`val` `div` `mod`	—	`add_comm` `mod_add_div`
`div_add_mod'` 📖	mathematical	—	`div` `val` `mod`	—	`mul_comm` `div_add_mod`
`dvd_antisymm` 📖	—	`PNat` `semigroupDvd` `Monoid.toSemigroup` `CommMonoid.toMonoid` `instCommMonoid`	—	—	`LE.le.antisymm` `le_of_dvd`
`dvd_iff` 📖	mathematical	—	`PNat` `semigroupDvd` `Monoid.toSemigroup` `CommMonoid.toMonoid` `instCommMonoid` `val`	—	`dvd_mul_right` `MulZeroClass.mul_zero` `mul_coe` `mk_coe`
`dvd_iff'` 📖	mathematical	—	`PNat` `semigroupDvd` `Monoid.toSemigroup` `CommMonoid.toMonoid` `instCommMonoid` `mod`	—	`dvd_iff` `eq` `mod_coe` `LT.lt.ne` `pos`
`dvd_one_iff` 📖	mathematical	—	`PNat` `semigroupDvd` `Monoid.toSemigroup` `CommMonoid.toMonoid` `instCommMonoid` `instOfNatPNatOfNeZeroNat`	—	`dvd_antisymm` `one_dvd` `dvd_refl`
`exists_eq_succ_of_ne_one` 📖	mathematical	—	`PNat` `instAddPNat` `instOfNatPNatOfNeZeroNat`	—	`IsRightCancelAdd.addRightStrictMono_of_addRightMono` `AddRightCancelSemigroup.toIsRightCancelAdd` `covariant_swap_add_of_covariant_add` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `contravariant_swap_add_of_contravariant_add` `contravariant_lt_of_covariant_le` `Nat.instCanonicallyOrderedAdd` `Nat.instZeroLEOneClass`
`instIsOrderedCancelMonoid` 📖	mathematical	—	`IsOrderedCancelMonoid` `PNat` `instCommMonoid` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `instLinearOrderPNat`	—	`Positive.isOrderedCancelMonoid` `Nat.instIsStrictOrderedRing`
`instWellFoundedLT` 📖	mathematical	—	`WellFoundedLT` `PNat` `Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `instLinearOrderPNat`	—	`WellFoundedRelation.isWellFounded`
`le_of_dvd` 📖	mathematical	`PNat` `semigroupDvd` `Monoid.toSemigroup` `CommMonoid.toMonoid` `instCommMonoid`	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `instLinearOrderPNat`	—	`dvd_iff'` `mod_le`
`le_one_iff` 📖	mathematical	—	`PNat` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `instLinearOrderPNat` `instOfNatPNatOfNeZeroNat`	—	`le_bot_iff`
`le_sub_one_of_lt` 📖	mathematical	`PNat` `Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `instLinearOrderPNat`	`Preorder.toLE` `instSub` `instOfNatPNatOfNeZeroNat`	—	`coe_le_coe` `sub_coe` `LE.le.trans` `LT.lt.le` `le_of_not_gt`
`lt_add_left` 📖	mathematical	—	`PNat` `Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `instLinearOrderPNat` `instAddPNat`	—	`lt_add_of_pos_left` `IsRightCancelAdd.addRightStrictMono_of_addRightMono` `AddRightCancelSemigroup.toIsRightCancelAdd` `covariant_swap_add_of_covariant_add` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid`
`lt_add_one_iff` 📖	mathematical	—	`PNat` `Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `instLinearOrderPNat` `instAddPNat` `instOfNatPNatOfNeZeroNat` `Preorder.toLE`	—	—
`lt_add_right` 📖	mathematical	—	`PNat` `Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `instLinearOrderPNat` `instAddPNat`	—	`LT.lt.trans_eq` `lt_add_left` `add_comm`
`lt_succ_self` 📖	mathematical	—	`PNat` `Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `instLinearOrderPNat` `Nat.succPNat` `val`	—	—
`mk_ofNat` 📖	mathematical	—	`PNat` `instOfNatPNatOfNeZeroNat` `MulZeroClass.toZero` `Nat.instMulZeroClass` `LT.lt.ne'` `Nat.instPreorder`	—	—
`modDivAux_spec` 📖	mathematical	—	`val` `PNat` `modDivAux`	—	`zero_add` `add_comm`
`mod_add_div` 📖	mathematical	—	`val` `mod` `div`	—	`ne_zero` `zero_add` `MulZeroClass.mul_zero` `modDivAux_spec`
`mod_add_div'` 📖	mathematical	—	`val` `mod` `div`	—	`mul_comm` `mod_add_div`
`mod_le` 📖	mathematical	—	`PNat` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `instLinearOrderPNat` `mod`	—	`mod_coe` `pos` `zero_add` `lt_irrefl` `MulZeroClass.mul_zero` `mul_one` `le_refl` `LT.lt.le`
`mul_coe` 📖	mathematical	—	`val` `PNat` `instMulPNat`	—	—
`mul_div_exact` 📖	mathematical	`PNat` `semigroupDvd` `Monoid.toSemigroup` `CommMonoid.toMonoid` `instCommMonoid`	`instMulPNat` `divExact`	—	`eq` `mul_coe` `div_add_mod` `dvd_iff'`
`natPred_add_one` 📖	mathematical	—	`natPred` `val`	—	`add_comm` `one_add_natPred`
`natPred_inj` 📖	mathematical	—	`natPred`	—	`natPred_injective`
`natPred_injective` 📖	mathematical	—	`PNat` `natPred`	—	`StrictMono.injective` `natPred_strictMono`
`natPred_le_natPred` 📖	mathematical	—	`natPred` `PNat` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `instLinearOrderPNat`	—	`StrictMono.le_iff_le` `natPred_strictMono`
`natPred_lt_natPred` 📖	mathematical	—	`natPred` `PNat` `Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `instLinearOrderPNat`	—	`StrictMono.lt_iff_lt` `natPred_strictMono`
`natPred_monotone` 📖	mathematical	—	`Monotone` `PNat` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `instLinearOrderPNat` `Nat.instPreorder` `natPred`	—	`StrictMono.monotone` `natPred_strictMono`
`natPred_strictMono` 📖	mathematical	—	`StrictMono` `PNat` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `instLinearOrderPNat` `Nat.instPreorder` `natPred`	—	`LT.lt.ne'`
`ofNat_inj` 📖	—	—	—	—	—
`ofNat_le_ofNat` 📖	mathematical	—	`PNat` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `instLinearOrderPNat`	—	—
`ofNat_lt_ofNat` 📖	mathematical	—	`PNat` `Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `instLinearOrderPNat`	—	—
`one_add_natPred` 📖	mathematical	—	`natPred` `val`	—	`natPred.eq_1` `add_tsub_cancel_iff_le` `Nat.instCanonicallyOrderedAdd` `Nat.instOrderedSub`
`one_lt_of_lt` 📖	mathematical	`PNat` `Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `instLinearOrderPNat`	`instOfNatPNatOfNeZeroNat`	—	`LE.le.trans_lt` `bot_le`
`pos_of_div_pos` 📖	—	`val`	—	—	`pos_iff_ne_zero` `Nat.instCanonicallyOrderedAdd` `ne_zero` `eq_zero_of_zero_dvd`
`pow_coe` 📖	mathematical	—	`val` `PNat` `Monoid.toNatPow` `CommMonoid.toMonoid` `instCommMonoid` `Nat.instMonoid`	—	—
`recOn_one` 📖	mathematical	—	`PNat` `instOfNatPNatOfNeZeroNat`	—	—
`recOn_succ` 📖	mathematical	—	`PNat` `instAddPNat` `instOfNatPNatOfNeZeroNat`	—	—
`sub_add_of_lt` 📖	mathematical	`PNat` `Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `instLinearOrderPNat`	`instAddPNat` `instSub`	—	`add_comm` `add_sub_of_lt`
`sub_coe` 📖	mathematical	—	`val` `PNat` `instSub` `Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `instLinearOrderPNat` `LinearOrder.toDecidableLT`	—	`toPNat'_coe` `tsub_pos_of_lt` `Nat.instCanonicallyOrderedAdd` `Nat.instOrderedSub` `tsub_eq_zero_iff_le` `le_of_not_gt`
`sub_le` 📖	mathematical	—	`PNat` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `instLinearOrderPNat` `instSub`	—	`coe_le_coe` `sub_coe`
`val_ofNat` 📖	mathematical	—	`val`	—	—

(root)

Definitions

Name	Category	Theorems
`instAddCommSemigroupPNat` 📖	CompOp	—
`instAddLeftCancelSemigroupPNat` 📖	CompOp	—
`instAddPNat` 📖	CompOp	20 math math: `PNat.addLeftMono`, `PNat.coeAddHom_apply`, `PNat.lt_add_right`, `PNat.addLeftReflectLT`, `PNat.add_sub`, `Mathlib.Tactic.Ring.instCSLiftValPNatNatHAdd`, `PNat.add_coe`, `PNat.add_one_le_iff`, `PNat.sub_add_of_lt`, `PNat.recOn_succ`, `PNat.succ_eq_add_one`, `PNat.addLeftReflectLE`, `PNat.lt_add_left`, `PNat.add_one`, `PNatPowAssoc.ppow_add`, `PNat.lt_add_one_iff`, `PNat.add_sub_of_lt`, `ppow_add`, `PNat.addLeftStrictMono`, `PNat.exists_eq_succ_of_ne_one`
`instAddRightCancelSemigroupPNat` 📖	CompOp	—
`instDistribPNat` 📖	CompOp	—
`instMulPNat` 📖	CompOp	32 math math: `PNat.factorMultiset_mul`, `PNat.gcd_b_eq`, `PNat.gcd_props`, `Mathlib.Tactic.Ring.instCSLiftValPNatNatHMul`, `PNat.Coprime.factor_eq_gcd_right_right`, `PNat.Coprime.gcd_mul_right_cancel`, `PNat.gcd_det_eq`, `PrimeMultiset.prod_add`, `PNat.Coprime.gcd_mul_right_cancel_right`, `PNat.Coprime.gcd_mul_left_cancel`, `PNat.equivNonZeroDivisorsNat_symm_apply_coe`, `PNat.gcd_rel_left'`, `PNat.Coprime.factor_eq_gcd_right`, `PNat.gcd_mul_lcm`, `ppow_mul'`, `PNat.Coprime.gcd_mul`, `PNat.equivNonZeroDivisorsNat_apply_coe`, `PNat.Coprime.mul`, `DivisibleHull.mk_add_mk`, `DivisibleHull.qsmul_mk`, `PNat.mul_coe`, `PNat.Coprime.factor_eq_gcd_left`, `ppow_mul`, `PrimeMultiset.prod_ofPNatList`, `PNat.gcd_rel_right'`, `PNat.Coprime.factor_eq_gcd_left_right`, `PNat.Coprime.gcd_mul_left_cancel_right`, `PNat.gcd_a_eq`, `PNat.Coprime.mul_right`, `ONote.oadd_mul`, `DivisibleHull.nnqsmul_mk`, `PNat.mul_div_exact`

---

← Back to Index