mathlib3
d8096aa6 - fix(ring_theory/subring): `inclusion` is a ring_hom! (#9849)

Commit

4 years ago

fix(ring_theory/subring): `inclusion` is a ring_hom! (#9849)

Author

jcommelin

jcommelin

Parents

Loading