mathlib3

d7f8f580 - feat(algebra/star/unitary): (re)define unitary elements of a star monoid (#11457)

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](https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/unitary.20submonoid) on Zulip. Co-authored-by: Eric Wieser <wieser.eric@gmail.com> Co-authored-by: Frédéric Dupuis <31101893+dupuisf@users.noreply.github.com>