Commit 2021-07-27 06:14 fb815d7b
View on Github →feat(algebra/ring/basic): coercions of ring_hom.id (#8439) Two basic lemmas about the identity map as a ring hom, split off from #3292 at @eric-wieser's suggestion.
feat(algebra/ring/basic): coercions of ring_hom.id (#8439) Two basic lemmas about the identity map as a ring hom, split off from #3292 at @eric-wieser's suggestion.