Commit 2022-01-16 15:00 d7f8f580

feat(algebra/star/unitary): (re)define unitary elements of a star monoid (#11457) This PR defines unitary R for a star monoid R as the submonoid containing the elements that satisfy both star U * U = 1 and U * star U = 1. We show basic properties (i.e. that this forms a group) and show that they preserve the norm when R is a C* ring. Note that this replaces unitary_submonoid, which only included the condition star U * U = 1 -- see the discussion on Zulip.