Additional instances for ring
over PNat
#
This adds some instances which enable ring
to work on PNat
even though it is not a commutative
semiring, by lifting to Nat
.
Equations
- Mathlib.Tactic.Ring.instCSLiftPNatNat = { lift := PNat.val, inj := PNat.coe_injective }