mathlib

69eed2f6 - feat(algebra/star/star_alg_hom): define `star_alg_equiv`s and provide basic API (#16784)

feat(algebra/star/star_alg_hom): define `star_alg_equiv`s and provide basic API (#16784) This defines `star_alg_equiv`'s in a way that is agnostic about whether the algebra is unital or non-unital, in much the same way as `ring_equiv` can handle both unital and non-unital rings. Currently, `alg_equiv` is not agnostic in this way, and even requires an `algebra` instance. The type class assumptions for `star_alg_equiv`, in contrast, are as minimal as possible, requiring only that the relevant operations `+, *, •, star` are defined. - [x] depends on: #16783