Commit 2025-04-18 13:26 06187a42

View on Github →

chore(PNat/Factors): get rid of Coe.coe (#24169)

Estimated changes

Modified Mathlib/Data/PNat/Factors.lean

modified theorem PrimeMultiset.coeNat_injective

modified theorem PrimeMultiset.coePNat_injective

modified theorem PrimeMultiset.coe_coeNatMonoidHom

modified theorem PrimeMultiset.coe_coePNatMonoidHom

modified def PrimeMultiset.toNatMultiset

modified def PrimeMultiset.toPNatMultiset