Commit 2025-05-16 11:26 7050e9f7

View on Github →

chore(MvPowerSeries,PNat): avoid Coe.coe (#24945) More along the lines of #24887

Estimated changes

Modified Mathlib/Data/PNat/Basic.lean

modified theorem PNat.coe_coeMonoidHom

Modified Mathlib/RingTheory/MvPowerSeries/Basic.lean

modified theorem MvPolynomial.coe_injective