mathlib

e1eb0bd9 - feat(algebra/algebra/unitization): add star structure for the unitization of a non-unital algebra (#13120)

feat(algebra/algebra/unitization): add star structure for the unitization of a non-unital algebra (#13120) The unitization of an algebra has a natural star structure when the underlying scalar ring and non-unital algebra have suitably interacting star structures. Co-authored-by: Frédéric Dupuis <dupuisf@iro.umontreal.ca>