Commit 2022-10-25 09:58 0d580447

View on Github →

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.

Estimated changes

Modified src/data/nat/prime.lean

modified theorem nat.primes.coe_nat_inj

added theorem nat.primes.coe_nat_injective

Modified src/data/pnat/basic.lean

modified theorem pnat.add_coe

modified theorem pnat.coe_bit0

modified theorem pnat.coe_bit1

modified theorem pnat.coe_eq_one_iff

modified theorem pnat.coe_inj

modified theorem pnat.mul_coe

modified theorem pnat.one_coe

modified theorem pnat.pow_coe

Modified src/data/pnat/factors.lean

Modified src/data/pnat/prime.lean

modified theorem nat.primes.coe_pnat_inj

added theorem nat.primes.coe_pnat_injective

modified theorem nat.primes.coe_pnat_nat

modified theorem pnat.gcd_coe

modified theorem pnat.lcm_coe