Commit 2023-02-06 07:13 948f2ea7

View on Github →

feat: port Data.PNat.Factors (#1830)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Data/Nat/Prime.lean

Modified Mathlib/Data/PNat/Basic.lean

modified theorem PNat.pow_coe

Created Mathlib/Data/PNat/Factors.lean

added theorem PNat.coeNat_factorMultiset

added theorem PNat.count_factorMultiset

added def PNat.factorMultiset

added def PNat.factorMultisetEquiv

added theorem PNat.factorMultiset_gcd

added theorem PNat.factorMultiset_lcm

added theorem PNat.factorMultiset_le_iff'

added theorem PNat.factorMultiset_le_iff

added theorem PNat.factorMultiset_mul

added theorem PNat.factorMultiset_ofPrime

added theorem PNat.factorMultiset_one

added theorem PNat.factorMultiset_pow

added theorem PNat.prod_factorMultiset

added theorem PrimeMultiset.card_ofPrime

added def PrimeMultiset.coeNatMonoidHom

added theorem PrimeMultiset.coeNat_injective

added theorem PrimeMultiset.coeNat_ofPrime

added theorem PrimeMultiset.coeNat_prime

added def PrimeMultiset.coePNatMonoidHom

added theorem PrimeMultiset.coePNat_injective

added theorem PrimeMultiset.coePNat_nat

added theorem PrimeMultiset.coePNat_ofPrime

added theorem PrimeMultiset.coePNat_prime

added theorem PrimeMultiset.coe_coeNatMonoidHom

added theorem PrimeMultiset.coe_coePNatMonoidHom

added theorem PrimeMultiset.coe_prod

added theorem PrimeMultiset.factorMultiset_prod

added def PrimeMultiset.ofNatList

added def PrimeMultiset.ofNatMultiset

added def PrimeMultiset.ofPNatList

added def PrimeMultiset.ofPNatMultiset

added def PrimeMultiset.ofPrime

added def PrimeMultiset.prod

added theorem PrimeMultiset.prod_add

added theorem PrimeMultiset.prod_dvd_iff'

added theorem PrimeMultiset.prod_dvd_iff

added theorem PrimeMultiset.prod_inf

added theorem PrimeMultiset.prod_ofNatList

added theorem PrimeMultiset.prod_ofNatMultiset

added theorem PrimeMultiset.prod_ofPNatList

added theorem PrimeMultiset.prod_ofPNatMultiset

added theorem PrimeMultiset.prod_ofPrime

added theorem PrimeMultiset.prod_smul

added theorem PrimeMultiset.prod_sup

added theorem PrimeMultiset.prod_zero

added def PrimeMultiset.toNatMultiset

added def PrimeMultiset.toPNatMultiset

added theorem PrimeMultiset.to_ofNatMultiset

added theorem PrimeMultiset.to_ofPNatMultiset

added def PrimeMultiset