basic): add ring_hom_ext' and move ext attribute to ring_hom_ext' (#9235)

Commit

4 years ago

chore(data/mv_polynomial/basic): add ring_hom_ext' and move ext attribute to ring_hom_ext' (#9235) Co-authored-by: Chris Hughes <33847686+ChrisHughes24@users.noreply.github.com>

Author

ChrisHughes24

Parents

10a62016

mathlib3 33db1c76 - chore(data/mv_polynomial/basic): add ring_hom_ext' and move ext attribute to ring_hom_ext' (#9235)

mathlib3
33db1c76 - chore(data/mv_polynomial/basic): add ring_hom_ext' and move ext attribute to ring_hom_ext' (#9235)