mathlib

7fdc06de - chore(data/nat/part_enat): make `coe_inj` `@[norm_cast]` (#16334)