`star_ring` then so is `Rᵒᵖ` (#9446)

Commit

4 years ago

feat(algebra/star): If `R` is a `star_monoid`/`star_ring` then so is `Rᵒᵖ` (#9446) The definition is simply that `op (star r) = star (op r)`

Author

eric-wieser

Parents