Mathlib v3 is deprecated. Go to Mathlib v4

Theorem part_enat.eq_coe_sub_of_add_eq_coe

Modification history

2023-02-27 10:42
src/data/nat/part_enat.lean
feat(data/nat/multiplicity): rename `nat.multiplicity_choose_prime_pow`, add lemmas (#18183) …
Added part_enat.eq_coe_sub_of_add_eq_coeView on Github →