mathlib
93bb4fbd - Add special-case `coe_one_hom` instance for `nat`

Commit

3 years ago

Add special-case `coe_one_hom` instance for `nat` Apparently ordinals are not enough of a ring to warrant a `coe_ring_hom` instance!

Author

Vierkantor

Committer

Vierkantor

Parents