Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-09-05 03:19 7fdc06de

View on Github →

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

Estimated changes

modified theorem part_enat.coe_inj