mathlib

709b4498 - chore(algebra/star/basic): provide automorphisms in commutative rings (#9483)

chore(algebra/star/basic): provide automorphisms in commutative rings (#9483) This adds `star_mul_aut` and `star_ring_aut`, which are the versions of `star_mul_equiv` and `star_ring_equiv` which avoid needing `opposite` due to commutativity.