basic): add ring_hom.has_involutive_star (#17904)

Commit

3 years ago

feat(algebra/star/basic): add ring_hom.has_involutive_star (#17904) Define an instance `has_involutive_star` for ring homorphisms into a `star_ring`.

Author

xroblot

Parents