Basic

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

Statistics

Metric	Count
Definitions `pnatIsoNat`, `caseStrongInductionOn`, `coeAddHom`, `coeMonoidHom`, `instCancelCommMonoid`, `instOrderBot`, `instSub`, `recOn`, `instAddCommSemigroupPNat`, `instAddLeftCancelSemigroupPNat`, `instAddLeftMonoPNat`, `instAddLeftReflectLEPNat`, `instAddLeftReflectLTPNat`, `instAddLeftStrictMonoPNat`, `instAddPNat`, `instAddRightCancelSemigroupPNat`, `instCommMonoidPNat`, `instDistribPNat`, `instIsOrderedCancelMonoidPNat`, `instMulPNat`, `instWellFoundedLTPNat`	21
Theorems `succPNat_inj`, `succPNat_injective`, `succPNat_le_succPNat`, `succPNat_lt_succPNat`, `succPNat_mono`, `succPNat_strictMono`, `pnatIsoNat_apply`, `pnatIsoNat_symm_apply`, `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`, `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`	58
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	—
`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
`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` `instIsRightCancelAddOfAddRightReflectLE` `contravariant_swap_add_of_contravariant_add` `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`	`PNat` `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` `instCommMonoidPNat` `Nat.instMulOneClass` `MonoidHom.instFunLike` `coeMonoidHom` `val`	—	—
`coe_inj` 📖	mathematical	—	`val`	—	—
`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` `instCommMonoidPNat`	—	—	`LE.le.antisymm` `le_of_dvd`
`dvd_iff` 📖	mathematical	—	`PNat` `semigroupDvd` `Monoid.toSemigroup` `CommMonoid.toMonoid` `instCommMonoidPNat` `val`	—	`dvd_mul_right` `MulZeroClass.mul_zero` `mul_coe` `mk_coe`
`dvd_iff'` 📖	mathematical	—	`PNat` `semigroupDvd` `Monoid.toSemigroup` `CommMonoid.toMonoid` `instCommMonoidPNat` `mod`	—	`dvd_iff` `eq` `mod_coe` `LT.lt.ne` `pos`
`dvd_one_iff` 📖	mathematical	—	`PNat` `semigroupDvd` `Monoid.toSemigroup` `CommMonoid.toMonoid` `instCommMonoidPNat` `instOfNatPNatOfNeZeroNat`	—	`dvd_antisymm` `one_dvd` `dvd_refl`
`exists_eq_succ_of_ne_one` 📖	mathematical	—	`PNat` `instAddPNat` `instOfNatPNatOfNeZeroNat`	—	`IsRightCancelAdd.addRightStrictMono_of_addRightMono` `instIsRightCancelAddOfAddRightReflectLE` `contravariant_swap_add_of_contravariant_add` `IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT` `instIsLeftCancelAddOfAddLeftReflectLE` `IsOrderedCancelAddMonoid.toAddLeftReflectLE` `Nat.instIsOrderedCancelAddMonoid` `contravariant_lt_of_covariant_le` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `covariant_swap_add_of_covariant_add` `Nat.instCanonicallyOrderedAdd` `Nat.instZeroLEOneClass`
`le_of_dvd` 📖	mathematical	`PNat` `semigroupDvd` `Monoid.toSemigroup` `CommMonoid.toMonoid` `instCommMonoidPNat`	`PNat` `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`	`PNat` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `instLinearOrderPNat` `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` `instIsRightCancelAddOfAddRightReflectLE` `contravariant_swap_add_of_contravariant_add` `IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT` `instIsLeftCancelAddOfAddLeftReflectLE` `IsOrderedCancelAddMonoid.toAddLeftReflectLE` `Nat.instIsOrderedCancelAddMonoid` `contravariant_lt_of_covariant_le` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `covariant_swap_add_of_covariant_add`
`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` `instCommMonoidPNat`	`PNat` `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`	`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.toPow` `CommMonoid.toMonoid` `instCommMonoidPNat` `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`	`PNat` `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	—
`instAddLeftMonoPNat` 📖	CompOp	—
`instAddLeftReflectLEPNat` 📖	CompOp	—
`instAddLeftReflectLTPNat` 📖	CompOp	—
`instAddLeftStrictMonoPNat` 📖	CompOp	—
`instAddPNat` 📖	CompOp	17 math math: `PNat.coeAddHom_apply`, `PNat.lt_add_right`, `PNat.add_sub`, `Mathlib.Tactic.Ring.instCSLiftValPNatNatHAdd`, `PNat.find_comp_succ`, `PNat.add_coe`, `PNat.add_one_le_iff`, `PNat.sub_add_of_lt`, `PNat.recOn_succ`, `PNat.succ_eq_add_one`, `PNat.lt_add_left`, `PNat.add_one`, `PNatPowAssoc.ppow_add`, `PNat.lt_add_one_iff`, `PNat.add_sub_of_lt`, `ppow_add`, `PNat.exists_eq_succ_of_ne_one`
`instAddRightCancelSemigroupPNat` 📖	CompOp	—
`instCommMonoidPNat` 📖	CompOp	28 math math: `PNat.lcm_dvd`, `PrimeMultiset.prod_dvd_prod`, `PNat.factorMultiset_le_iff`, `PrimeMultiset.prod_dvd_iff'`, `PNat.Prime.not_dvd_one`, `PNat.dvd_lcm_right`, `PNat.gcd_dvd_right`, `PNat.dvd_one_iff`, `PNat.gcd_eq_right_iff_dvd`, `PNat.count_factorMultiset`, `PNat.factorMultiset_le_iff'`, `PNat.dvd_gcd`, `PNat.dvd_iff`, `PNat.exists_prime_and_dvd`, `PrimeMultiset.prod_dvd_iff`, `PNat.dvd_lcm_left`, `PrimeMultiset.prod_ofPNatMultiset`, `PNat.gcd_dvd_left`, `PNat.dvd_prime`, `PNat.factorMultiset_pow`, `PNat.pow_coe`, `PNat.dvd_iff'`, `Mathlib.Tactic.Ring.instCSLiftValPNatNatHPow`, `PNat.mem_factorMultiset`, `PrimeMultiset.prod_smul`, `Finset.PNat.coe_prod`, `PNat.gcd_eq_left_iff_dvd`, `PNat.coe_coeMonoidHom`
`instDistribPNat` 📖	CompOp	—
`instIsOrderedCancelMonoidPNat` 📖	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`
`instWellFoundedLTPNat` 📖	CompOp	—

---

← Back to Index