mathlib3

0d580447 - feat(data/pnat): add missing `norm_cast` attributes (#16995)

feat(data/pnat): add missing `norm_cast` attributes (#16995) Also renames `nat.primes.coe_[p]nat_inj` to `nat.primes.coe_[p]nat_injective` to match the naming guide, and make room for the `iff` version occupying the original name.