-
Notifications
You must be signed in to change notification settings - Fork 298
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
[Merged by Bors] - feat(algebra/star/unitary): (re)define unitary elements of a star monoid #11457
Conversation
I went ahead and pushed my golfing suggestions, since it was easier than adding github comments - hope that's ok! |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
LGTM, but since I pushed some golfs someone else should take a quick look (as should you, of course!)
(@eric-wieser it seems your golfs broke the build) |
Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
Thanks -- the changes look good! |
Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
bors d+
Thanks!
✌️ dupuisf can now approve this pull request. To approve and merge a pull request, simply reply with |
Co-authored-by: sgouezel <sebastien.gouezel@univ-rennes1.fr>
bors r+ |
…oid (#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>
Pull request successfully merged into master. Build succeeded: |
This PR defines
unitary R
for a star monoidR
as the submonoid containing the elements that satisfy bothstar U * U = 1
andU * star U = 1
. We show basic properties (i.e. that this forms a group) and show that theypreserve the norm when
R
is a C* ring.Note that this replaces
unitary_submonoid
, which only included the conditionstar U * U = 1
-- see the discussion on Zulip.