Factors

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

Statistics

Metric	Count
Definitions `factorMultiset`, `factorMultisetEquiv`, `PrimeMultiset`, `coeMultisetPNatNat`, `coeNat`, `coeNatMonoidHom`, `coePNat`, `coePNatMonoidHom`, `instRepr`, `ofNatList`, `ofNatMultiset`, `ofPNatList`, `ofPNatMultiset`, `ofPrime`, `prod`, `toNatMultiset`, `toPNatMultiset`, `instAddCommMonoidPrimeMultiset`, `instCanonicallyOrderedAddPrimeMultiset`, `instDistribLatticePrimeMultiset`, `instInhabitedPrimeMultiset`, `instIsOrderedCancelAddMonoidPrimeMultiset`, `instOrderBotPrimeMultiset`, `instOrderedSubPrimeMultiset`, `instSemilatticeSupPrimeMultiset`, `instSubPrimeMultiset`	26
Theorems `coeNat_factorMultiset`, `count_factorMultiset`, `factorMultiset_gcd`, `factorMultiset_lcm`, `factorMultiset_le_iff`, `factorMultiset_le_iff'`, `factorMultiset_mono`, `factorMultiset_mul`, `factorMultiset_ofPrime`, `factorMultiset_one`, `factorMultiset_pow`, `mem_factorMultiset`, `prod_factorMultiset`, `card_ofPrime`, `coeNat_injective`, `coeNat_ofPrime`, `coeNat_prime`, `coePNat_injective`, `coePNat_nat`, `coePNat_ofPrime`, `coePNat_prime`, `coe_coeNatMonoidHom`, `coe_coePNatMonoidHom`, `coe_prod`, `factorMultiset_prod`, `mem_ofNatList`, `mem_ofNatMultiset`, `prod_add`, `prod_dvd_iff`, `prod_dvd_iff'`, `prod_dvd_prod`, `prod_inf`, `prod_ofNatList`, `prod_ofNatMultiset`, `prod_ofPNatList`, `prod_ofPNatMultiset`, `prod_ofPrime`, `prod_smul`, `prod_sup`, `prod_zero`, `toPNatMultiset_ofPNatList`, `to_ofNatMultiset`, `to_ofPNatMultiset`	43
Total	69

PNat

Definitions

Name	Category	Theorems
`factorMultiset` 📖	CompOp	15 math math: `factorMultiset_mul`, `factorMultiset_le_iff`, `PrimeMultiset.prod_dvd_iff'`, `count_factorMultiset`, `factorMultiset_gcd`, `factorMultiset_le_iff'`, `factorMultiset_ofPrime`, `factorMultiset_mono`, `factorMultiset_pow`, `factorMultiset_one`, `factorMultiset_lcm`, `PrimeMultiset.factorMultiset_prod`, `coeNat_factorMultiset`, `prod_factorMultiset`, `mem_factorMultiset`
`factorMultisetEquiv` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coeNat_factorMultiset` 📖	mathematical	—	`PrimeMultiset.toNatMultiset` `factorMultiset` `Multiset.ofList` `Nat.primeFactorsList` `val`	—	`PrimeMultiset.to_ofNatMultiset` `Nat.prime_of_mem_primeFactorsList`
`count_factorMultiset` 📖	mathematical	—	`PNat` `semigroupDvd` `Monoid.toSemigroup` `CommMonoid.toMonoid` `instCommMonoid` `Monoid.toNatPow` `Nat.Primes.toPNat` `Multiset.count` `Nat.Primes` `Nat.instDecidableEqPrimes` `factorMultiset`	—	`Multiset.le_count_iff_replicate_le` `factorMultiset_le_iff` `factorMultiset_pow` `factorMultiset_ofPrime` `Multiset.eq_replicate` `Multiset.card_nsmul` `PrimeMultiset.card_ofPrime` `mul_one` `Multiset.eq_of_mem_replicate` `Multiset.nsmul_singleton` `PrimeMultiset.ofPrime.eq_1`
`factorMultiset_gcd` 📖	mathematical	—	`factorMultiset` `gcd` `PrimeMultiset` `SemilatticeInf.toMin` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticePrimeMultiset`	—	`le_antisymm` `le_inf_iff` `factorMultiset_le_iff` `gcd_dvd_left` `gcd_dvd_right` `PrimeMultiset.prod_dvd_iff` `prod_factorMultiset` `dvd_gcd` `PrimeMultiset.prod_dvd_iff'` `inf_le_left` `inf_le_right`
`factorMultiset_lcm` 📖	mathematical	—	`factorMultiset` `lcm` `PrimeMultiset` `SemilatticeSup.toMax` `instSemilatticeSupPrimeMultiset`	—	`le_antisymm` `PrimeMultiset.prod_dvd_iff` `prod_factorMultiset` `lcm_dvd` `factorMultiset_le_iff'` `le_sup_left` `le_sup_right` `sup_le_iff` `factorMultiset_le_iff` `dvd_lcm_left` `dvd_lcm_right`
`factorMultiset_le_iff` 📖	mathematical	—	`PrimeMultiset` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticePrimeMultiset` `factorMultiset` `PNat` `semigroupDvd` `Monoid.toSemigroup` `CommMonoid.toMonoid` `instCommMonoid`	—	`prod_factorMultiset` `Dvd.intro` `PrimeMultiset.prod_add` `PrimeMultiset.factorMultiset_prod` `add_tsub_cancel_of_le` `CanonicallyOrderedAdd.toExistsAddOfLE` `IsOrderedAddMonoid.toAddLeftMono` `IsOrderedCancelAddMonoid.toIsOrderedAddMonoid` `mul_div_exact` `factorMultiset_mul` `le_self_add`
`factorMultiset_le_iff'` 📖	mathematical	—	`PrimeMultiset` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticePrimeMultiset` `factorMultiset` `PNat` `semigroupDvd` `Monoid.toSemigroup` `CommMonoid.toMonoid` `instCommMonoid` `PrimeMultiset.prod`	—	`factorMultiset_le_iff` `PrimeMultiset.factorMultiset_prod`
`factorMultiset_mono` 📖	mathematical	`PNat` `semigroupDvd` `Monoid.toSemigroup` `CommMonoid.toMonoid` `instCommMonoid`	`PrimeMultiset` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticePrimeMultiset` `factorMultiset`	—	`factorMultiset_le_iff`
`factorMultiset_mul` 📖	mathematical	—	`factorMultiset` `PNat` `instMulPNat` `PrimeMultiset` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `instAddCommMonoidPrimeMultiset`	—	`prod_factorMultiset` `PrimeMultiset.prod_add` `PrimeMultiset.factorMultiset_prod`
`factorMultiset_ofPrime` 📖	mathematical	—	`factorMultiset` `Nat.Primes.toPNat` `PrimeMultiset.ofPrime`	—	`Equiv.injective` `prod_factorMultiset` `PrimeMultiset.prod_ofPrime`
`factorMultiset_one` 📖	mathematical	—	`factorMultiset` `PNat` `instOfNatPNatOfNeZeroNat` `PrimeMultiset` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `instAddCommMonoidPrimeMultiset`	—	`Multiset.pmap.congr_simp` `Nat.primeFactorsList_one`
`factorMultiset_pow` 📖	mathematical	—	`factorMultiset` `PNat` `Monoid.toNatPow` `CommMonoid.toMonoid` `instCommMonoid` `PrimeMultiset` `AddMonoid.toNatSMul` `AddCommMonoid.toAddMonoid` `instAddCommMonoidPrimeMultiset`	—	`prod_factorMultiset` `PrimeMultiset.prod_smul` `PrimeMultiset.factorMultiset_prod`
`mem_factorMultiset` 📖	mathematical	—	`PNat` `Multiset` `Multiset.instMembership` `PrimeMultiset.toPNatMultiset` `factorMultiset` `Prime` `semigroupDvd` `Monoid.toSemigroup` `CommMonoid.toMonoid` `instCommMonoid`	—	—
`prod_factorMultiset` 📖	mathematical	—	`PrimeMultiset.prod` `factorMultiset`	—	`eq` `PrimeMultiset.prod_ofNatList` `Nat.prod_primeFactorsList` `ne_zero`

PrimeMultiset

Definitions

Name	Category	Theorems
`coeMultisetPNatNat` 📖	CompOp	—
`coeNat` 📖	CompOp	—
`coeNatMonoidHom` 📖	CompOp	1 math math: `coe_coeNatMonoidHom`
`coePNat` 📖	CompOp	—
`coePNatMonoidHom` 📖	CompOp	1 math math: `coe_coePNatMonoidHom`
`instRepr` 📖	CompOp	—
`ofNatList` 📖	CompOp	2 math math: `prod_ofNatList`, `mem_ofNatList`
`ofNatMultiset` 📖	CompOp	3 math math: `mem_ofNatMultiset`, `prod_ofNatMultiset`, `to_ofNatMultiset`
`ofPNatList` 📖	CompOp	2 math math: `toPNatMultiset_ofPNatList`, `prod_ofPNatList`
`ofPNatMultiset` 📖	CompOp	2 math math: `prod_ofPNatMultiset`, `to_ofPNatMultiset`
`ofPrime` 📖	CompOp	5 math math: `prod_ofPrime`, `PNat.factorMultiset_ofPrime`, `coePNat_ofPrime`, `coeNat_ofPrime`, `card_ofPrime`
`prod` 📖	CompOp	17 math math: `prod_ofNatList`, `prod_dvd_prod`, `prod_dvd_iff'`, `prod_add`, `PNat.factorMultiset_le_iff'`, `prod_ofPrime`, `prod_inf`, `prod_dvd_iff`, `prod_sup`, `prod_ofPNatMultiset`, `prod_ofPNatList`, `prod_zero`, `factorMultiset_prod`, `PNat.prod_factorMultiset`, `prod_ofNatMultiset`, `prod_smul`, `coe_prod`
`toNatMultiset` 📖	CompOp	7 math math: `coePNat_nat`, `coe_coeNatMonoidHom`, `PNat.coeNat_factorMultiset`, `coeNat_injective`, `coeNat_ofPrime`, `to_ofNatMultiset`, `coe_prod`
`toPNatMultiset` 📖	CompOp	9 math math: `toPNatMultiset_ofPNatList`, `coe_coePNatMonoidHom`, `mem_ofNatMultiset`, `coePNat_nat`, `to_ofPNatMultiset`, `coePNat_ofPrime`, `PNat.mem_factorMultiset`, `coePNat_injective`, `mem_ofNatList`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`card_ofPrime` 📖	mathematical	—	`Multiset.card` `Nat.Primes` `ofPrime`	—	—
`coeNat_injective` 📖	mathematical	—	`PrimeMultiset` `Multiset` `toNatMultiset`	—	`Multiset.map_injective` `Nat.Primes.coe_nat_injective`
`coeNat_ofPrime` 📖	mathematical	—	`toNatMultiset` `ofPrime` `Multiset` `Multiset.instSingleton` `Nat.Prime`	—	—
`coeNat_prime` 📖	mathematical	`Multiset` `Multiset.instMembership` `toNatMultiset`	`Nat.Prime`	—	`Multiset.mem_map`
`coePNat_injective` 📖	mathematical	—	`PrimeMultiset` `Multiset` `PNat` `toPNatMultiset`	—	`Multiset.map_injective` `Nat.Primes.coe_pnat_injective`
`coePNat_nat` 📖	mathematical	—	`Multiset.map` `PNat` `PNat.val` `toPNatMultiset` `toNatMultiset`	—	`Multiset.map_map`
`coePNat_ofPrime` 📖	mathematical	—	`toPNatMultiset` `ofPrime` `PNat` `Multiset` `Multiset.instSingleton` `Nat.Primes.toPNat`	—	—
`coePNat_prime` 📖	mathematical	`PNat` `Multiset` `Multiset.instMembership` `toPNatMultiset`	`PNat.Prime`	—	`Multiset.mem_map`
`coe_coeNatMonoidHom` 📖	mathematical	—	`DFunLike.coe` `AddMonoidHom` `PrimeMultiset` `Multiset` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `instAddCommMonoidPrimeMultiset` `AddCancelCommMonoid.toAddCommMonoid` `Multiset.instAddCancelCommMonoid` `AddMonoidHom.instFunLike` `coeNatMonoidHom` `toNatMultiset`	—	—
`coe_coePNatMonoidHom` 📖	mathematical	—	`DFunLike.coe` `AddMonoidHom` `PrimeMultiset` `Multiset` `PNat` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `instAddCommMonoidPrimeMultiset` `AddCancelCommMonoid.toAddCommMonoid` `Multiset.instAddCancelCommMonoid` `AddMonoidHom.instFunLike` `coePNatMonoidHom` `toPNatMultiset`	—	—
`coe_prod` 📖	mathematical	—	`PNat.val` `prod` `Multiset.prod` `Nat.instCommMonoid` `toNatMultiset`	—	`MonoidHom.map_multiset_prod` `Multiset.map_map` `Multiset.map_congr`
`factorMultiset_prod` 📖	mathematical	—	`PNat.factorMultiset` `prod`	—	`coeNat_injective` `PNat.coeNat_factorMultiset` `coe_prod` `Multiset.coe_eq_coe` `Nat.primeFactorsList_unique`
`mem_ofNatList` 📖	mathematical	`Nat.Prime`	`PNat` `Multiset` `Multiset.instMembership` `toPNatMultiset` `ofNatList` `PNat.val`	—	—
`mem_ofNatMultiset` 📖	mathematical	`Nat.Prime`	`PNat` `Multiset` `Multiset.instMembership` `toPNatMultiset` `ofNatMultiset` `PNat.val`	—	`Multiset.map_congr` `Multiset.map_pmap`
`prod_add` 📖	mathematical	—	`prod` `PrimeMultiset` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `instAddCommMonoidPrimeMultiset` `PNat` `instMulPNat`	—	`AddMonoidHom.map_add` `Multiset.prod_add`
`prod_dvd_iff` 📖	mathematical	—	`PNat` `semigroupDvd` `Monoid.toSemigroup` `CommMonoid.toMonoid` `PNat.instCommMonoid` `prod` `PrimeMultiset` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticePrimeMultiset`	—	`PNat.factorMultiset_le_iff'` `factorMultiset_prod`
`prod_dvd_iff'` 📖	mathematical	—	`PNat` `semigroupDvd` `Monoid.toSemigroup` `CommMonoid.toMonoid` `PNat.instCommMonoid` `prod` `PrimeMultiset` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticePrimeMultiset` `PNat.factorMultiset`	—	`prod_dvd_iff` `PNat.prod_factorMultiset`
`prod_dvd_prod` 📖	mathematical	`PrimeMultiset` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticePrimeMultiset`	`PNat` `semigroupDvd` `Monoid.toSemigroup` `CommMonoid.toMonoid` `PNat.instCommMonoid` `prod`	—	`prod_dvd_iff`
`prod_inf` 📖	mathematical	—	`prod` `PrimeMultiset` `SemilatticeInf.toMin` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticePrimeMultiset` `PNat.gcd`	—	`factorMultiset_prod` `PNat.factorMultiset_gcd` `PNat.prod_factorMultiset`
`prod_ofNatList` 📖	mathematical	`Nat.Prime`	`PNat.val` `prod` `ofNatList` `Nat.instOne`	—	`prod_ofNatMultiset` `Multiset.prod_coe`
`prod_ofNatMultiset` 📖	mathematical	`Nat.Prime`	`PNat.val` `prod` `ofNatMultiset` `Multiset.prod` `Nat.instCommMonoid`	—	`coe_prod` `to_ofNatMultiset`
`prod_ofPNatList` 📖	mathematical	`PNat.Prime`	`prod` `ofPNatList` `PNat` `instMulPNat` `instOnePNat`	—	`prod_ofPNatMultiset` `Multiset.prod_coe`
`prod_ofPNatMultiset` 📖	mathematical	`PNat.Prime`	`prod` `ofPNatMultiset` `Multiset.prod` `PNat` `PNat.instCommMonoid`	—	`to_ofPNatMultiset`
`prod_ofPrime` 📖	mathematical	—	`prod` `ofPrime` `Nat.Primes.toPNat`	—	`Multiset.prod_singleton`
`prod_smul` 📖	mathematical	—	`prod` `PrimeMultiset` `AddMonoid.toNatSMul` `AddCommMonoid.toAddMonoid` `instAddCommMonoidPrimeMultiset` `PNat` `Monoid.toNatPow` `CommMonoid.toMonoid` `PNat.instCommMonoid`	—	`zero_nsmul` `prod_zero` `pow_zero` `succ_nsmul` `prod_add` `pow_succ`
`prod_sup` 📖	mathematical	—	`prod` `PrimeMultiset` `SemilatticeSup.toMax` `instSemilatticeSupPrimeMultiset` `PNat.lcm`	—	`factorMultiset_prod` `PNat.factorMultiset_lcm` `PNat.prod_factorMultiset`
`prod_zero` 📖	mathematical	—	`prod` `PrimeMultiset` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `instAddCommMonoidPrimeMultiset` `PNat` `instOfNatPNatOfNeZeroNat`	—	`Multiset.prod_zero`
`toPNatMultiset_ofPNatList` 📖	mathematical	`PNat.Prime`	`toPNatMultiset` `ofPNatList` `Multiset.ofList` `PNat`	—	`to_ofPNatMultiset`
`to_ofNatMultiset` 📖	mathematical	`Nat.Prime`	`toNatMultiset` `ofNatMultiset`	—	`Multiset.map_pmap` `Multiset.pmap_eq_map` `Multiset.map_id'`
`to_ofPNatMultiset` 📖	mathematical	`PNat.Prime`	`toPNatMultiset` `ofPNatMultiset`	—	`Multiset.map_pmap` `Multiset.pmap_eq_map` `Multiset.map_id`

(root)

Definitions

Name	Category	Theorems
`PrimeMultiset` 📖	CompOp	19 math math: `PNat.factorMultiset_mul`, `PNat.factorMultiset_le_iff`, `PrimeMultiset.prod_dvd_iff'`, `PrimeMultiset.prod_add`, `PNat.factorMultiset_gcd`, `PNat.factorMultiset_le_iff'`, `PrimeMultiset.prod_inf`, `PrimeMultiset.prod_dvd_iff`, `PNat.factorMultiset_mono`, `PrimeMultiset.coe_coePNatMonoidHom`, `PrimeMultiset.prod_sup`, `PNat.factorMultiset_pow`, `PNat.factorMultiset_one`, `PrimeMultiset.coe_coeNatMonoidHom`, `PNat.factorMultiset_lcm`, `PrimeMultiset.prod_zero`, `PrimeMultiset.prod_smul`, `PrimeMultiset.coeNat_injective`, `PrimeMultiset.coePNat_injective`
`instAddCommMonoidPrimeMultiset` 📖	CompOp	8 math math: `PNat.factorMultiset_mul`, `PrimeMultiset.prod_add`, `PrimeMultiset.coe_coePNatMonoidHom`, `PNat.factorMultiset_pow`, `PNat.factorMultiset_one`, `PrimeMultiset.coe_coeNatMonoidHom`, `PrimeMultiset.prod_zero`, `PrimeMultiset.prod_smul`
`instCanonicallyOrderedAddPrimeMultiset` 📖	CompOp	—
`instDistribLatticePrimeMultiset` 📖	CompOp	7 math math: `PNat.factorMultiset_le_iff`, `PrimeMultiset.prod_dvd_iff'`, `PNat.factorMultiset_gcd`, `PNat.factorMultiset_le_iff'`, `PrimeMultiset.prod_inf`, `PrimeMultiset.prod_dvd_iff`, `PNat.factorMultiset_mono`
`instInhabitedPrimeMultiset` 📖	CompOp	—
`instIsOrderedCancelAddMonoidPrimeMultiset` 📖	CompOp	—
`instOrderBotPrimeMultiset` 📖	CompOp	—
`instOrderedSubPrimeMultiset` 📖	CompOp	—
`instSemilatticeSupPrimeMultiset` 📖	CompOp	2 math math: `PrimeMultiset.prod_sup`, `PNat.factorMultiset_lcm`
`instSubPrimeMultiset` 📖	CompOp	—

---

← Back to Index