mathlib

ca0ff3ad - feat(algebra/algebra/spectrum): show the star and spectrum operations commute (#12351)

feat(algebra/algebra/spectrum): show the star and spectrum operations commute (#12351) This establishes the identity `(σ a)⋆ = σ a⋆` for any `a : A` where `A` is a star ring and a star module over a star add monoid `R`.